Theorem merlem10

Step 19 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 \theta \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
meredith
\( \vdash (((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \neg \varphi \rightarrow \neg \theta) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \theta \rightarrow \varphi \rightarrow \psi \)
merlem9
\( \vdash ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \neg \varphi \rightarrow \neg \theta) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \theta \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 \theta \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 \theta \rightarrow \varphi \rightarrow \psi \)
ax-mp l0 _