Theorem 3anbi3d

Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis
3anbi1d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \wedge \tau \wedge \psi \leftrightarrow \theta \wedge \tau \wedge \chi) \)
Proof
l0
biidd
3anbi1d.1
3anbi13d l0 _