Question: I'm reading [Wikipedia](https://en.wikipedia.org/wiki/Hilbert_system) 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: 
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.
> 
> 
>
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.