Theorem 3anbi1i

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