Hilbert System Logical Axiom 1 follows from Axioms 2 and 3

Question

I'm reading Wikipedia and it lists the first four logical axioms that allow (together with modus ponens) for the manipulation of logical connectives.

1. $\phi \to \phi $
2. $\phi \to \left(\psi \to \phi \right)$
3. $\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$
4. $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$

Then it states "The axiom 1 is redundant, as it follows from 3, 2 and modus ponens."

I see that if I substitute (2) into (3), I get

$$\left(\phi \to \left(\psi \rightarrow \phi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \phi \right)\right)$$

Since (2) is true, modus ponens tells me

$$\left(\phi \to \psi \right)\to \left(\phi \to \phi \right)$$

So (1) would be true if I knew that $\left(\phi \to \psi \right)$ is true. But how do I know that?

If there's a better way to do this proof than the way I approached it, I'll also accept that answer.

Answer 1

Hint: Remember you get to pick what $\psi$ is. Is there any formula $\psi$ such that you know $(\phi\to\psi)$ is true?

More details are hidden below.

By axiom 2, if you choose $\psi$ to have the form $(\psi'\to\phi)$ for some formula $\psi'$, then you know $(\phi\to \psi)$ is true.

Answer 2

By (3) we have $$ (\phi\to((\phi\to\phi)\to\phi))\to((\phi\to(\phi\to\phi))\to(\phi\to\phi)) $$ By (2), $$ \phi\to ((\phi\to\phi)\to\phi) $$ So $$ ((\phi\to(\phi\to\phi))\to(\phi\to\phi)) $$ by Modus Ponens.

By (2), $$ \phi\to (\phi\to\phi) $$ so $$ \phi\to\phi $$ by Modus Ponens again.