Theorem merlem5
Step 11 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 \psi) \rightarrow \neg \neg \varphi \rightarrow \psi \)
Proof
l0
meredith
\( \vdash ((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi \)
l1
meredith
\( \vdash ((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \neg \neg \varphi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi \)
l2
merlem1
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi) \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \neg \varphi \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi) \)
merlem4
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi) \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \neg \varphi \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow (((((\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi) \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \neg \varphi \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \neg \neg \varphi) \rightarrow \psi) \rightarrow \varphi \)
l4
ax-mp l2 _
\( \vdash (((((\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi) \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \neg \varphi \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \neg \neg \varphi) \rightarrow \psi) \rightarrow \varphi \)
meredith
\( \vdash ((((((\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi) \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \neg \varphi \rightarrow \neg (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi)) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \neg \neg \varphi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \neg \neg \varphi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi) \rightarrow (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi \)
ax-mp l4 _
\( \vdash (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \neg \neg \varphi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi) \rightarrow (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi \)
ax-mp l1 _
\( \vdash (((((\psi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \psi) \rightarrow \psi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \neg \neg \varphi \rightarrow \psi \)
ax-mp l0 _