Theorem merlem13
Step 35 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 ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \psi \)
Proof
l0
merlem12
\( \vdash ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \)
l1
merlem12
\( \vdash ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi \)
merlem5
\( \vdash (((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi \)
l3
ax-mp l1 _
\( \vdash \neg \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi \)
merlem6
\( \vdash (\neg \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow (((\neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow \neg \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow (\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \)
l5
ax-mp l3 _
\( \vdash (((\neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow \neg \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow (\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \)
meredith
\( \vdash ((((\neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow \neg \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow (\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow (((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \)
ax-mp l5 _
\( \vdash (((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \)
l8
ax-mp l0 _
\( \vdash \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \)
merlem6
\( \vdash (\neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow \varphi \)
l10
ax-mp l8 _
\( \vdash (((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow \varphi \)
merlem11
\( \vdash ((((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow \varphi \)
l12
ax-mp l10 _
\( \vdash (((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow \varphi \)
meredith
\( \vdash ((((\psi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \neg ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi)) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\theta \rightarrow \neg \neg \chi \rightarrow \chi) \rightarrow \neg \neg \varphi) \rightarrow \psi \)
ax-mp l12 _