Theorem merlem3
Step 7 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 ((\psi \rightarrow \chi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
Proof
l0
merlem2
\( \vdash ((\neg \chi \rightarrow \neg \chi) \rightarrow \neg \chi \rightarrow \neg \chi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi \)
merlem2
\( \vdash (((\neg \chi \rightarrow \neg \chi) \rightarrow \neg \chi \rightarrow \neg \chi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi \)
l2
ax-mp l0 _
\( \vdash (((\chi \rightarrow \varphi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi \)
meredith
\( \vdash ((((\chi \rightarrow \varphi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
l4
ax-mp l2 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
meredith
\( \vdash ((((\varphi \rightarrow \varphi) \rightarrow \neg \chi \rightarrow \neg \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
ax-mp l4 _