# Metamath Proof Explorer

## Theorem merco1lem14

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 merco1lem14 ${⊢}\left(\left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\to {\chi }\right)\to \left({\phi }\to {\chi }\right)$

### Proof

Step Hyp Ref Expression
1 merco1lem13 ${⊢}\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)$
2 merco1lem8 ${⊢}\left(\left(\left(\left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to {\phi }\right)\to \left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \perp \right)\right)\to {\phi }\right)\to \left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)$
3 merco1 ${⊢}\left(\left(\left(\left(\left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to {\phi }\right)\to \left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \perp \right)\right)\to {\phi }\right)\to \left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\right)$
4 2 3 ax-mp ${⊢}\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)$
5 merco1lem9 ${⊢}\left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\right)\to \left(\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)$
6 4 5 ax-mp ${⊢}\left(\left(\left(\left({\phi }\to {\psi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\right)\to \left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)$
7 1 6 ax-mp ${⊢}{\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)$
8 merco1lem12 ${⊢}\left({\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left(\left(\left({\chi }\to {\phi }\right)\to \left({\phi }\to \perp \right)\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)$
9 7 8 ax-mp ${⊢}\left(\left(\left({\chi }\to {\phi }\right)\to \left({\phi }\to \perp \right)\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)$
10 merco1 ${⊢}\left(\left(\left(\left({\chi }\to {\phi }\right)\to \left({\phi }\to \perp \right)\right)\to {\phi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\right)\to \left(\left(\left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\to {\chi }\right)\to \left({\phi }\to {\chi }\right)\right)$
11 9 10 ax-mp ${⊢}\left(\left(\left({\phi }\to {\psi }\right)\to {\psi }\right)\to {\chi }\right)\to \left({\phi }\to {\chi }\right)$