Prove the following theorem in propositional calculus I have the following Hilbert-style propositional calculus, having the logical connectives $\{\neg,\rightarrow\}$ of arity one and two respectively, and the following axioms:
A1: $A\rightarrow(B\rightarrow A)$
A2: $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))$
A3: $(\neg A\rightarrow \neg B)\rightarrow (B\rightarrow A).$
$A,B,C$ are any well-formed formulas (wffs). The only inference rule is modus ponens. I want to prove the following theorem:
$\vdash (\neg A\rightarrow A)\rightarrow A$ for any wff $A$.
You may use any or all of the following theorems without proof:
$\vdash A\rightarrow A$ for any wff $A$.
$A\rightarrow B, B\rightarrow C\vdash A\rightarrow C$ for any wffs $A,B,C$.
$A\rightarrow (B\rightarrow C), B\vdash A\rightarrow C$ for any wffs $A,B,C$.
$\vdash \neg A\rightarrow (A\rightarrow B)$ for any wffs $A,B$.
Please avoid using the deduction theorem unless absolutely necessary.

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

5) $\vdash (\lnot A \to A) \to (B \to A)$ --- from 3) and 4) by Th.2

Proof
1) $\vdash (\lnot A \to A) \to ((\lnot A \to A) \to A)$ --- from Lemma
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)
4) $\vdash (\lnot A \to A) \to (\lnot A \to A)$ --- from Th.1

5) $\vdash (\lnot A \to A) \to A$ --- from 3) and 4)

