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 φ θ ψ θ χ


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 φ θ ψ θ χ