How to prove $\vdash p\to\neg\neg p$ in this system?

Question

I was asked to prove $\vdash p\to\neg\neg p$ in this system.

Axioms:
$(\mathcal A_1)\vdash p\to(q\to p)$
$(\mathcal A_2)\vdash (p\to(q\to r))\to((p\to q)\to (p\to r))$
$(\mathcal A_3)\vdash \neg\neg p\to p$

I have tried to use axiom 2 and find a proper proposition $x$ such that $\vdash (p\to(x\to\neg\neg p)) \to ((p\to x)\to (p\to \neg\neg p))$ holds, but I couldn't find one.

Any help would be appreciated.

Note from a comment on a deleted answer: there is also a rule that $\lnot P$ may be replaced by $P \to \bot$.

Answer 1

Okay.. I've known how to solve this — by employing the Deduction Theorem:

If $A$ is a set of propositions, $p$, $q$ are propositions, then $A \vdash p\to q$ is equivalent to $A \cup \{p\} \vdash q$.

Proof

$$\{p,\neg p\}\vdash p\tag{1; assumed}$$ $$\{p,\neg p\}\vdash \neg p=(p\to\bot)\tag{2; assumed}$$ $$\{p,\neg p\}\vdash \bot\quad\tag{3; MP,1,2}$$ $$\{p\}\vdash (\neg p\to \bot)=\neg\neg p\tag{4; DT}$$ $$\vdash (p\to \neg\neg p)\tag{5; DT}$$