I was asked to prove $\vdash p\to\neg\neg p$ in this system.
$(\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$.