Metamath Proof Explorer


Theorem anbi12i

Description: Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypotheses anbi12.1 φ ψ
anbi12.2 χ θ
Assertion anbi12i φ χ ψ θ

Proof

Step Hyp Ref Expression
1 anbi12.1 φ ψ
2 anbi12.2 χ θ
3 2 anbi2i φ χ φ θ
4 3 1 bianbi φ χ ψ θ