Metamath Proof Explorer


Theorem mercolem8

Description: Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 . (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion mercolem8 φ ψ ψ φ χ τ θ φ χ

Proof

Step Hyp Ref Expression
1 merco2 φ φ φ φ φ φ φ φ φ
2 merco2 φ χ φ ψ φ ψ ψ φ χ τ θ φ χ
3 mercolem3 φ χ φ ψ φ ψ ψ φ χ τ θ φ χ φ χ φ ψ φ ψ φ ψ ψ φ χ τ θ φ χ
4 2 3 ax-mp φ χ φ ψ φ ψ φ ψ ψ φ χ τ θ φ χ
5 mercolem7 φ ψ φ χ φ ψ φ ψ
6 mercolem7 φ ψ φ χ φ ψ φ ψ φ ψ ψ φ χ τ θ φ χ φ φ χ φ ψ φ ψ φ φ χ φ ψ φ ψ
7 5 6 ax-mp φ ψ ψ φ χ τ θ φ χ φ φ χ φ ψ φ ψ φ φ χ φ ψ φ ψ
8 merco2 φ ψ ψ φ χ τ θ φ χ φ φ χ φ ψ φ ψ φ φ χ φ ψ φ ψ φ χ φ ψ φ ψ φ ψ ψ φ χ τ θ φ χ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ ψ ψ φ χ τ θ φ χ
9 7 8 ax-mp φ χ φ ψ φ ψ φ ψ ψ φ χ τ θ φ χ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ ψ ψ φ χ τ θ φ χ
10 4 9 ax-mp φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ ψ ψ φ χ τ θ φ χ
11 1 10 ax-mp φ φ φ φ φ φ φ φ φ φ ψ ψ φ χ τ θ φ χ
12 1 11 ax-mp φ ψ ψ φ χ τ θ φ χ