Theorem 3anbi3i

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 \theta \wedge \varphi \leftrightarrow \chi \wedge \theta \wedge \psi \)
Proof
l0
biid
l1
biid
3anbi1i.1
3anbi123i l0 l1 _