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.
 A: 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)

A: 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}

