Finding a derivation of $\vdash{(\lnot\lnot{p}\to{p})}$ I'm reading through Derek Goldrei's "Propositional and Predicate Calculus" book and I've come across an exercise problem that states to show the derivation of "$\vdash{(\lnot\lnot{p}\to{p})}$" using these three axioms:
$$(\phi\to{(\psi\to{\phi}))}$$
$$((\phi\to{(\psi\to{\theta}))}\to{((\phi\to{\psi})\to{(\psi\to{\theta})})}$$
$$((\lnot\phi\to{\lnot\psi})\to{(\psi\to{\phi})})$$
As well as the deduction theorem. I searched through Stack Exchange and found some answers. However, the note the author gives states:

Our private solution includes use of Ax 1, Ax 3, Modus Ponens, and the deduction theorem.

And so far every solution posted here contains solutions that either use lemmas not yet introduced, or the use of other axioms. My question is how would one derive the formula using only the first and third axiom, modus ponens, and the deduction theorem only. This is what I have so far:
$$\begin{align}
&(0)\quad\vdash{(\lnot\lnot{p}\to{p})}&&\text{. . .}\\
&(1)\quad\lnot\lnot{p}\vdash{p}&&\text{Deduction Theorem}\\
\\
&(2)\quad\lnot\lnot{p}&&\text{Assumption}\\
&(3)\quad(\lnot\lnot{p}\to{(p\to{\lnot\lnot{p}})})&&\text{Ax 1}\\
&(4)\quad(p\to{\lnot\lnot{p}})&&\text{MP 2, 3}
\end{align}
$$
I just feel stuck as to where to go next, or if I even started off correctly. A solution is not required, just a step in the right direction could help. 
 A: Hint 1:

 Derive the Principle of Explosion, i.e. $p,\neg p\vdash q$.

Hint 2:

 You would be done if you could prove $\neg p\to\neg\neg\neg p$ via Ax3 and Modus Ponens.

Hint 3:

 To prove $\neg p\to\neg\neg\neg p$, you will use essentially the Principle of Explosion.

Here's a natural deduction proof.

 $$\dfrac{\dfrac{\dfrac{}{\vdash (\neg p\to\neg\neg\neg p)\to(\neg\neg p\to p)}{\tiny\text{Ax}3}\quad\dfrac{\mathcal D}{\neg\neg p\vdash \neg p\to\neg\neg\neg p}{\tiny\to\!I}}{\neg\neg p\vdash \neg\neg p\to p}{\tiny\to\! E}\quad\dfrac{}{\neg\neg p\vdash\neg\neg p}}{\dfrac{\neg\neg p\vdash p}{\vdash\neg\neg p\to p}{\tiny\to\!I}}{\tiny\to\! E}$$ 

where $\mathcal D$ is the derivation

$$\dfrac{\dfrac{}{\vdash(\neg\neg\neg\neg p\to\neg\neg p)\to(\neg p\to \neg\neg\neg p)}{\tiny\text{Ax}3}\quad\dfrac{\dfrac{}{\vdash\neg\neg p\to(\neg\neg\neg\neg p\to \neg\neg p)}{\tiny\text{Ax}1}\quad\dfrac{}{\neg\neg p\vdash\neg\neg p}}{\neg\neg p\vdash\neg\neg\neg\neg p\to \neg\neg p}{\tiny\to\!E}}{\neg\neg p\vdash \neg p\to\neg\neg\neg p}{\tiny\to\!E}$$
$\mathcal D$ is basically a most of a proof of the principle of explosion. We have $\neg\neg p$ and $\neg p$ which clearly contradict each other from which we can infer anything, and in this case that is $\neg\neg\neg p$.

Uses of $\to\! I$ correspond to uses of the Deduction Theorem, and uses of $\to\! E$ correspond to Modus Ponens.
Presenting the above in a more Hilbert-style:

    1. Assume $\neg\neg p$.
    2. $\neg\neg p\to(\neg\neg\neg\neg p\to\neg\neg p)$ via Ax1.
    3. $\neg\neg\neg\neg p\to\neg\neg p$ via MP with 2 and 1.
    4. $(\neg\neg\neg\neg p\to\neg\neg p)\to(\neg p\to\neg\neg\neg p)$ via Ax3.
    5. $\neg p\to\neg\neg\neg p$ via MP with 4 and 3.
    6. $(\neg p\to\neg\neg\neg p)\to(\neg\neg p\to p)$ via Ax3.
    7. $\neg\neg p\to p$ via MP with 6 and 5.
    8. $p$ via MP with 7 and 1.
    9. $\neg\neg p\to p$ via Deduction Theorem discharging 1.

