Metamath Proof Explorer

Theorem anbi12d

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

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


Step Hyp Ref Expression
1 anbi12d.1 φ ψ χ
2 anbi12d.2 φ θ τ
3 1 anbi1d φ ψ θ χ θ
4 2 anbi2d φ χ θ χ τ
5 3 4 bitrd φ ψ θ χ τ