Theorem merlem7
Between steps 14 and 15 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 ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta \)
Proof
l0
merlem4
\( \vdash (\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta \)
l1
merlem6
\( \vdash (((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow \neg \varphi) \rightarrow \neg \chi \rightarrow \neg \varphi \)
meredith
\( \vdash ((((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow \neg \varphi) \rightarrow \neg \chi \rightarrow \neg \varphi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow \neg \varphi) \rightarrow \neg \chi \rightarrow \neg \varphi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
l3
ax-mp l1 _
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow \neg \varphi) \rightarrow \neg \chi \rightarrow \neg \varphi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
meredith
\( \vdash (((((((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow \neg \varphi) \rightarrow \neg \chi \rightarrow \neg \varphi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta \)
ax-mp l3 _
\( \vdash ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow ((\chi \rightarrow \tau) \rightarrow \neg \theta \rightarrow \neg \psi) \rightarrow \theta \)
ax-mp l0 _