Theorem merco1lem17
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 \varphi) \rightarrow \chi) \rightarrow \tau) \rightarrow (\varphi \rightarrow \chi) \rightarrow \tau \)
Proof
l0
merco1lem11
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
l1
merco1lem7
\( \vdash (((((((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow \bot) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
merco1
\( \vdash ((((((((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow \bot) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
l3
ax-mp l1 _
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
merco1lem9
\( \vdash (((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
ax-mp l3 _
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
l6
ax-mp l0 _
\( \vdash (((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
merco1
\( \vdash ((((\chi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
l8
ax-mp l6 _
\( \vdash (\varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
l9
merco1lem11
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi \)
l10
merco1lem7
\( \vdash ((((((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1
\( \vdash (((((((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi \)
l12
ax-mp l10 _
\( \vdash (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi \)
merco1lem9
\( \vdash ((((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi \)
ax-mp l12 _
\( \vdash (((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi \)
l15
ax-mp l9 _
\( \vdash ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi \)
merco1
\( \vdash (((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
ax-mp l15 _
\( \vdash ((\varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
l18
ax-mp l8 _
\( \vdash (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
merco1lem16
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
l20
ax-mp l18 _
\( \vdash (((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
l21
merco1lem4
\( \vdash (((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi \)
merco1lem11
\( \vdash ((((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi \)
l23
ax-mp l21 _
\( \vdash ((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi \)
merco1
\( \vdash (((((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow (((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
ax-mp l23 _
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow (((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
l26
ax-mp l20 _
\( \vdash (((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \)
merco1
\( \vdash ((((\tau \rightarrow \varphi) \rightarrow (\varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi) \rightarrow \tau) \rightarrow (\varphi \rightarrow \chi) \rightarrow \tau \)
ax-mp l26 _