Metamath Proof Explorer

Theorem bibi2d

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 19-May-2013)

Ref Expression
Hypothesis imbid.1 ⊢ φ → ψ ↔ χ
Assertion bibi2d ⊢ φ → θ ↔ ψ ↔ θ ↔ χ

Proof

Step Hyp Ref Expression
1 imbid.1 ⊢ φ → ψ ↔ χ
2 1 pm5.74i ⊢ φ → ψ ↔ φ → χ
3 2 bibi2i ⊢ φ → θ ↔ φ → ψ ↔ φ → θ ↔ φ → χ
4 pm5.74 ⊢ φ → θ ↔ ψ ↔ φ → θ ↔ φ → ψ
5 pm5.74 ⊢ φ → θ ↔ χ ↔ φ → θ ↔ φ → χ
6 3 4 5 3bitr4i ⊢ φ → θ ↔ ψ ↔ φ → θ ↔ χ
7 6 pm5.74ri ⊢ φ → θ ↔ ψ ↔ θ ↔ χ