Theorem merlem9
Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \eta \rightarrow \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau \)
Proof
l0
merlem6
\( \vdash (\theta \rightarrow \psi \rightarrow \tau) \rightarrow ((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta \)
merlem8
\( \vdash ((\theta \rightarrow \psi \rightarrow \tau) \rightarrow ((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow (((\psi \rightarrow \tau) \rightarrow \neg (\neg (((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \neg \theta) \rightarrow \neg \varphi) \rightarrow \neg (((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \neg \theta) \rightarrow ((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta \)
l2
ax-mp l0 _
\( \vdash (((\psi \rightarrow \tau) \rightarrow \neg (\neg (((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \neg \theta) \rightarrow \neg \varphi) \rightarrow \neg (((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \neg \theta) \rightarrow ((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta \)
meredith
\( \vdash ((((\psi \rightarrow \tau) \rightarrow \neg (\neg (((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \neg \theta) \rightarrow \neg \varphi) \rightarrow \neg (((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \neg \theta) \rightarrow ((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow ((((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
l4
ax-mp l2 _
\( \vdash ((((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
meredith
\( \vdash (((((\chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \neg \eta) \rightarrow \neg \psi \rightarrow \neg \eta) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau) \rightarrow \eta \rightarrow \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau \)
ax-mp l4 _