Theorem merco1lem2

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