Proving (A → -A) → -A In a Hilbert system Trying to prove (A → -A) → -A with the following axioms:
A → (B → A)
(A → (B → C)) → ((A → B) → (A → C))
(-A → -B) → (B → A)
Not an axiom, but you can also use A → (-A → B), which I've already managed to prove it.
Intuitively the proposition makes sense, but I'm not sure how to prove it
 A: Hint
With Ax.1 and Ax.2 you have to derive some preliminary useful results : 

$\vdash A \to A$ and the derived rule Syll : $A \to B, B \to C \vdash A \to C$,

and eventually the Deduction Theorem.
Then, Ax.3 is crucial in deriving double negation laws: 

$\vdash \lnot \lnot A \to A$ and : $\vdash A \to \lnot \lnot A$.

Double negation, in turn, give us : $\vdash (A \to B) \to (\lnot B \to \lnot A)$.

Two further Lemma :
1) $\vdash \lnot A \to (\lnot B \to \lnot A)$ --- Ax.1
2) $\vdash (\lnot B \to \lnot A) \to (A \to B)$ --- Ax.3

(A) $\vdash \lnot A \to (A \to B)$ --- from 1) and 2) by Syll


1) $\vdash \lnot A \to (A \to \lnot B)$ --- Lemma (A)
2) $\vdash (\lnot A \to (A \to \lnot B)) \to ((\lnot A \to A) \to (\lnot A \to B))$ --- Ax.2 
3) $\vdash (\lnot A \to A) \to (\lnot A \to B)$ --- from 1) and 2) by MP
4) $\vdash (\lnot A \to \lnot B) \to (B \to A)$ --- Ax.3

(B) $\vdash (\lnot A \to A) \to (B \to A)$ --- from 3) and 4) by Syll


1) $\vdash (\lnot A \to A) \to ((\lnot A \to A) \to A)$ --- Lemma (B)
2) $\vdash ((\lnot A \to A) \to ((\lnot A \to A) \to A)) \to (((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A))$ --- Ax.2 
3) $\vdash ((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A)$ --- from 1) and 2) by MP
4) $\vdash (\lnot A \to A) \to (\lnot A \to A)$ --- from $\vdash A \to A$ above

(C) $\vdash (\lnot A \to A) \to A$ --- from 3) and 4) by MP.



Now the proof :
1) $\vdash (\lnot \lnot A \to \lnot A) \to \lnot A$ --- Lemma (C)
2) $A \to \lnot A$ --- assumed [a]
3) $\lnot \lnot A \to \lnot A$ --- from 2)
4) $\lnot A$ --- from 1) and 3) by MP


5) $\vdash (A \to \lnot A) \to \lnot A$ --- from 2) and 4) by DT, discharging [a].


