Theorem merco1lem18
Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1.
(Contributed by Anthony Hart, 18-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
Proof
l0
merco1
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \bot) \rightarrow (\psi \rightarrow \chi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
merco1lem17
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \bot) \rightarrow (\psi \rightarrow \chi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
l2
ax-mp l0 _
\( \vdash (((\psi \rightarrow \chi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
merco1lem17
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
l4
ax-mp l2 _
\( \vdash (\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
l5
merco1lem5
\( \vdash (((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot \)
merco1lem3
\( \vdash ((((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot \)
l7
ax-mp l5 _
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot \)
merco1lem5
\( \vdash (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot \)
l9
ax-mp l7 _
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot \)
merco1lem4
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot \)
l11
ax-mp l9 _
\( \vdash ((\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot \)
l12
merco1
\( \vdash ((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \psi \rightarrow \varphi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
merco1lem2
\( \vdash (((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \psi \rightarrow \varphi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
ax-mp l12 _
\( \vdash (((\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
l15
ax-mp l11 _
\( \vdash ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
merco1lem9
\( \vdash (((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
ax-mp l15 _
\( \vdash ((\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
ax-mp l4 _