Theorem merco1lem3
Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1.
(Contributed by Anthony Hart, 17-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi \)
Proof
l0
merco1lem2
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \bot \)
l1
retbwax2
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi \)
merco1lem2
\( \vdash ((((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi \)
ax-mp l1 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi \)
l4
ax-mp l0 _
\( \vdash \varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi \)
l5
merco1lem2
\( \vdash ((\chi \rightarrow \varphi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \bot \)
l6
retbwax2
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi) \rightarrow (\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi \)
merco1lem2
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi) \rightarrow (\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi) \rightarrow (((\chi \rightarrow \varphi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \bot) \rightarrow (\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi \)
ax-mp l6 _
\( \vdash (((\chi \rightarrow \varphi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \bot) \rightarrow (\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi \)
ax-mp l5 _
\( \vdash (\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \chi \rightarrow \varphi \)
ax-mp l4 _