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 1 anbi1i φχψχ
4 2 anbi2i ψχψθ
5 3 4 bitri φχψθ