Theorem merlem1

Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.) (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\chi \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \tau) \rightarrow \varphi \rightarrow \tau \)
Proof
l0
meredith
\( \vdash ((((\neg \varphi \rightarrow \psi) \rightarrow \neg (\neg \tau \rightarrow \neg \chi) \rightarrow \neg \neg (\neg \varphi \rightarrow \psi)) \rightarrow \neg \tau \rightarrow \neg \chi) \rightarrow \tau) \rightarrow (\tau \rightarrow \neg \varphi) \rightarrow \neg (\neg \varphi \rightarrow \psi) \rightarrow \neg \varphi \)
meredith
\( \vdash (((((\neg \varphi \rightarrow \psi) \rightarrow \neg (\neg \tau \rightarrow \neg \chi) \rightarrow \neg \neg (\neg \varphi \rightarrow \psi)) \rightarrow \neg \tau \rightarrow \neg \chi) \rightarrow \tau) \rightarrow (\tau \rightarrow \neg \varphi) \rightarrow \neg (\neg \varphi \rightarrow \psi) \rightarrow \neg \varphi) \rightarrow (((\tau \rightarrow \neg \varphi) \rightarrow \neg (\neg \varphi \rightarrow \psi) \rightarrow \neg \varphi) \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \chi \rightarrow \neg \varphi \rightarrow \psi \)
l2
ax-mp l0 _
\( \vdash (((\tau \rightarrow \neg \varphi) \rightarrow \neg (\neg \varphi \rightarrow \psi) \rightarrow \neg \varphi) \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \chi \rightarrow \neg \varphi \rightarrow \psi \)
meredith
\( \vdash ((((\tau \rightarrow \neg \varphi) \rightarrow \neg (\neg \varphi \rightarrow \psi) \rightarrow \neg \varphi) \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \chi \rightarrow \neg \varphi \rightarrow \psi) \rightarrow ((\chi \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \tau) \rightarrow \varphi \rightarrow \tau \)
ax-mp l2 _