Theorem merco1lem15

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 \psi \)
Proof
l0
merco1lem14
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \rightarrow \psi \)
merco1lem13
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \rightarrow \psi \)
ax-mp l0 _