Theorem 3anbi2i

Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)

Hypothesis
3anbi1i.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \chi \wedge \varphi \wedge \theta \leftrightarrow \chi \wedge \psi \wedge \theta \)
Proof
l0
biid
l1
3anbi1i.1
biid
3anbi123i l0 l1 _