# Metamath Proof Explorer

## Theorem merco1lem13

Description: 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.)

Ref Expression
Assertion merco1lem13 ${⊢}\left(\left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\to {\tau }\right)\to \left({\phi }\to {\tau }\right)$

### Proof

Step Hyp Ref Expression
1 merco1 ${⊢}\left(\left(\left(\left({\psi }\to {\phi }\right)\to \left({\chi }\to \perp \right)\right)\to {\phi }\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)$
2 merco1lem4 ${⊢}\left(\left(\left(\left(\left({\psi }\to {\phi }\right)\to \left({\chi }\to \perp \right)\right)\to {\phi }\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\right)$
3 1 2 ax-mp ${⊢}{\phi }\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)$
4 merco1lem12 ${⊢}\left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\right)\to \left(\left(\left(\left({\tau }\to {\phi }\right)\to \left({\phi }\to \perp \right)\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\right)$
5 3 4 ax-mp ${⊢}\left(\left(\left({\tau }\to {\phi }\right)\to \left({\phi }\to \perp \right)\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)$
6 merco1 ${⊢}\left(\left(\left(\left({\tau }\to {\phi }\right)\to \left({\phi }\to \perp \right)\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\right)\to \left(\left(\left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\to {\tau }\right)\to \left({\phi }\to {\tau }\right)\right)$
7 5 6 ax-mp ${⊢}\left(\left(\left({\phi }\to {\psi }\right)\to \left({\chi }\to {\psi }\right)\right)\to {\tau }\right)\to \left({\phi }\to {\tau }\right)$