Metamath Proof Explorer


Theorem merco1lem5

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

Ref Expression
Assertion merco1lem5 φ χ τ φ τ

Proof

Step Hyp Ref Expression
1 merco1lem4 τ φ φ χ φ χ
2 merco1 τ φ φ χ φ χ φ χ τ φ τ
3 1 2 ax-mp φ χ τ φ τ