This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bibi12i

Description: The equivalence of two equivalences. (Contributed by NM, 26-May-1993)

Ref Expression
Hypotheses bibi2i.1 ⊢ φ ↔ ψ
bibi12i.2 ⊢ χ ↔ θ
Assertion bibi12i ⊢ φ ↔ χ ↔ ψ ↔ θ

Proof

Step Hyp Ref Expression
1 bibi2i.1 ⊢ φ ↔ ψ
2 bibi12i.2 ⊢ χ ↔ θ
3 2 bibi2i ⊢ φ ↔ χ ↔ φ ↔ θ
4 1 bibi1i ⊢ φ ↔ θ ↔ ψ ↔ θ
5 3 4 bitri ⊢ φ ↔ χ ↔ ψ ↔ θ