Metamath Proof Explorer

Theorem bibi2i

Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 16-May-2013)

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

Proof

Step Hyp Ref Expression
1 bibi2i.1 ⊢ φ ↔ ψ
2 id ⊢ χ ↔ φ → χ ↔ φ
3 2 1 bitrdi ⊢ χ ↔ φ → χ ↔ ψ
4 id ⊢ χ ↔ ψ → χ ↔ ψ
5 4 1 bitr4di ⊢ χ ↔ ψ → χ ↔ φ
6 3 5 impbii ⊢ χ ↔ φ ↔ χ ↔ ψ