Metamath Proof Explorer

Theorem bibi12d

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993)

Ref Expression
Hypotheses imbi12d.1 φ ψ χ
imbi12d.2 φ θ τ
Assertion bibi12d φ ψ θ χ τ


Step Hyp Ref Expression
1 imbi12d.1 φ ψ χ
2 imbi12d.2 φ θ τ
3 1 bibi1d φ ψ θ χ θ
4 2 bibi2d φ χ θ χ τ
5 3 4 bitrd φ ψ θ χ τ