Metamath Proof Explorer

Theorem imbi12d

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

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


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