I don't trust my proof of $ \neg ( \phi \rightarrow \neg \psi) \vdash \phi$

Question

I have just given an axiomatic proof of conjunction elimination, but I don't trust it. I wonder if anyone will take a look. Note that $ \phi$ $\wedge$ $\psi$ is viewed here as an abbreviation of $\neg (\phi \rightarrow \neg \psi)$. I am allowed the following axioms plus any derived rules, and I have derived $\neg \neg$E, $\rightarrow$I and $\phi$,$\neg \phi$ $\vdash \psi$ (EFQ) myself:

$(A1) \hspace{0.1cm}\phi \rightarrow (\psi \rightarrow \phi)\ $

$(A2)\hspace{0.1cm} \phi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))\ $

$(A3)\hspace{0.1cm}(\neg \phi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \phi) $

1. $\neg (\phi \rightarrow \neg \psi)\hspace{2cm}$ Premise
2. $\neg \phi \hspace{3.5cm}$ assumption
3. $\phi \hspace{3.75cm}$ assumption
4. $\neg \psi \hspace{3.4cm}$ Ex falso Quodlibet
5. $\phi \rightarrow \neg \psi \hspace{2.35cm}$ Conditional Intro
6. $ \neg \neg \phi \hspace{3.1cm}$ Negation Intro
7. $\phi \hspace{3.6cm}$ Double-negation Elim

So I suppose $\neg \phi$ and $\phi$, derive $\neg \psi$ by EFQ, and then discharge $\phi$ to get $\phi \rightarrow \neg \psi$, which contradicts my premise, so I discharge $\neg \phi$ and get $\neg \neg \phi$. The rest is straightforward.