Proof in Propositional Logic of Peirce's Law How can I proove in Propositional Logic (using only the basic axioms of P.L. and not a valuation function like it's used in Propositional Calculus) that :

$\vdash$ ((($\phi$ $\to$ $\psi$ )$\to$ $\phi$)$\to$ $\phi$)

where $\phi$,$\psi$ are given formulas ?
 A: Axioms :
(A1) $\phi\to (\psi \to \phi)$
(A2) $(\phi → (ψ → ω)) → ((ϕ → ψ) → (ϕ → ω))$
(A3) $(\lnot ϕ → \lnot ψ) → ((\lnot ϕ → ψ) → ϕ)$.

With (A1) and (A2) we can prove :
Lemma 1 : $\vdash (\phi\to \phi)$.
With (A1), (A2) and Lemma 1 we can prove the:
Deduction Th : If $\Gamma$ is a set of formulae and $\phi, \psi$ are formulae, and $\Gamma , \phi \vdash \psi$, then $\Gamma \vdash \phi \to \psi$.
Finally, we have to prove :
Lemma 2 : $\vdash \lnot \phi \to (\phi \to \psi)$
1) $\lnot \phi$ --- premise
2) $\phi$ --- premise
3) $\vdash \phi \to (\lnot \psi \to \phi)$ --- (A1)
4) $\vdash \lnot \phi \to (\lnot \psi \to \lnot \phi)$ --- (A1)
5) $\lnot \psi \to \phi$ --- from 2) and 3) by modus ponens
6) $\lnot \psi \to \lnot \phi$ --- from 1) and 4) by mp
7) $\psi$ --- from 5), 6) and (A3)

8) $\lnot \phi, \phi \vdash \psi$ --- 1), 2) and 7)

$\vdash \lnot \phi \to (\phi \to \psi)$ --- from 8) by Ded.Th twice.



Now for the main proof :
1) $(ϕ → ψ) → ϕ$ --- premise
2) $\lnot \phi$ --- premise
3) $\vdash \lnot \phi \to (\phi \to \psi)$ --- Lemma 2
4) $\phi \to \psi$ --- from 2) and 3) by mp
5) $\phi$ --- from 1) and 4) by mp
6) $(ϕ → ψ) → ϕ \vdash \lnot \phi \to \phi$ --- from 2) and 5) by Ded.Th 
7) $\vdash \lnot \phi \to \lnot \phi$ --- Lemma 1
8) $(ϕ → ψ) → ϕ \vdash \phi$ --- from 6), 7) and (A3) by mp twice


$\vdash ((ϕ → ψ ) → ϕ) → ϕ$ --- from 8) by Ded.Th.


A: Using  form of natural deduction in which implication is left associative:

