Prove ⊢(a→b)→(¬b→¬a) in HPC proof system As stated in the title, I am asked to give a proof that:
⊢(a→b)→(¬b→¬a)
Using a system with the Modus Ponens rule, and the following axioms:


*

*A1: a→(b→a)

*A2: (a→(b→c))→((a→b)→(a→c))

*A3: (¬b→¬a)→(a→b)


According to the deduction theorem, it is sufficient to prove:
{(a→b), ¬b} ⊢ ¬a
Using the A3 I am managing at "removing" ¬'s, but cannot think of a way to add ¬'s.
Thank you very much for you help.
 A: We have to prove some preliminary results :
0) $\vdash a \to a$
1) $a \to b, b \to c \vdash a \to c$ (use Deduction Th)
2) $\vdash \lnot \lnot a \to a$ (use 1. and axiom A3)
3) $\vdash a \to \lnot \lnot a$ (use 2. and axiom A3).
Now :
i) $a \to b$
ii) $\vdash b \to \lnot \lnot b$
iii) $a \to \lnot \lnot b$ (with 1. above)
iv) $\vdash \lnot \lnot a \to a$
v) $\lnot \lnot a \to \lnot \lnot b$ (with 1. above)
vi) $\lnot b \to \lnot a$ (with A3)

$\vdash (a \to b) \to (\lnot b \to \lnot a)$ (from i. and vi. by Ded Th).


Proof of 2) :
i) $\vdash \lnot a \to (\lnot b \to \lnot a)$ (axiom A1)
ii) $\vdash (\lnot b \to \lnot a) \to (a \to b)$ (axiom A3)
iii) $\vdash \lnot a \to (a \to b)$ (with 1.)
iv) $\vdash \lnot \lnot a \to (\lnot a \to \lnot \lnot \lnot a)$ (from iii.)
v) $\vdash (\lnot a \to \lnot \lnot \lnot a) \to (\lnot \lnot a \to a)$ (axiom A3)
vi) $\vdash \lnot \lnot a \to (\lnot \lnot a \to a)$ (with 1.)
vii) $\vdash (\lnot \lnot a \to (\lnot \lnot a \to a)) \to ((\lnot \lnot a \to \lnot \lnot a) \to (\lnot \lnot a \to a))$ (axiom A2)

viii) $\vdash (\lnot \lnot a \to a)$ (with vi. and 0. above, by modus ponens twice).


Proof of 3) :
i) $\vdash \lnot \lnot \lnot a \to \lnot a$ (from 1.)
ii) $\vdash (\lnot \lnot \lnot a \to \lnot a) \to (a \to \lnot \lnot a)$ (axiom A3)

iii) $\vdash (a \to \lnot \lnot a)$ (by modus ponens).

