Theorem merlem11

Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
Proof
l0
meredith
\( \vdash ((((\varphi \rightarrow \varphi) \rightarrow \neg \varphi \rightarrow \neg \varphi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
l1
merlem10
\( \vdash (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
merlem10
\( \vdash ((\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow \neg \varphi \rightarrow \neg \varphi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
ax-mp l1 _
\( \vdash (((((\varphi \rightarrow \varphi) \rightarrow \neg \varphi \rightarrow \neg \varphi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
ax-mp l0 _