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

Metamath Proof Explorer

Theorem bibi1i

Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993)

Ref Expression
Hypothesis bibi2i.1 ⊢ φ ↔ ψ
Assertion bibi1i ⊢ φ ↔ χ ↔ ψ ↔ χ

Proof

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