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)
I use Polish notation.  Thus, instead I'll translate every wff of the form $\lnot$$\alpha$ into the form N$\alpha$.  Also, I'll translate every wff of the form ($\alpha$$\rightarrow$$\beta$) into the form C$\alpha$$\beta$.  Thus, the axioms can get translated to
A1 CxCyx
A2 CCxCyzCCxyCxz
A3 CCNxNyCxy
I'll also use spacing to help to indicate where a substitution of an axiom or previously proved theorem took place.

1 CxCyx
2 CCxCyzCCxyCxz
3 CCNxNyCyx
4 C CxCyx C z CxCyx from 1
5 CzCxCyx from {4, 1}
6 CC CxCyz C Cxy Cxz CC CxCyz Cxy C CxCyz Cxz from 2
7 CCCxCyzCxyCCxCyzCxz from {6, 2}
8 C CCNxNyCyx C z CCNxNyCyx from 1
9 CzCCNxNyCyx from {8, 3}
10 C CxCCyxz C x C y x from 5
11 CCC x C Cyx z C x Cyx CC x C Cyx z C x z from 7
12 CCxCCyxzCxz from {11, 10}
13 CC z C CNxNy Cyx CC z CNxNy C z Cyx from 2
14 CCzCNxNyCzCyx from {13, 9}
15 CC Nz CC Ny Nz Czy C Nz Czy from 12
16 C Nz CC Ny Nz C z y from 9
17 CNzCzy from {15, 16}
18 CC Nz C z y CC Nz z C Nz y from 2
19 CCNzzCNzy from {18, 17}
20 CC CNzz CN z N y C CNzz C y z from 14
21 CCN z z CN z Ny from 19
22 CCNzzCyz from {20, 21}
23 CC CNxx CC y CNxx x C CNxx x from 12
24 CCN x x C CyCNxx x from 22
25 CCNxxx from {23, 24}