Theorem merco1lem13
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 \tau) \rightarrow \varphi \rightarrow \tau \)
Proof
l0
merco1
\( \vdash ((((\psi \rightarrow \varphi) \rightarrow \chi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
merco1lem4
\( \vdash (((((\psi \rightarrow \varphi) \rightarrow \chi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
l2
ax-mp l0 _
\( \vdash \varphi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
merco1lem12
\( \vdash (\varphi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\tau \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
l4
ax-mp l2 _
\( \vdash (((\tau \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
merco1
\( \vdash ((((\tau \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow \tau) \rightarrow \varphi \rightarrow \tau \)
ax-mp l4 _