# Hilbert System Logical Axiom 1 follows from Axioms 2 and 3

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.

Hint: Remember you get to pick what $$\psi$$ is. Is there any formula $$\psi$$ such that you know $$(\phi\to\psi)$$ is true?
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.
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.