Theorem merco1lem10

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