Theorem anbi2d

Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis
anbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \wedge \psi \leftrightarrow \theta \wedge \chi) \)
Proof
anbid.1
a1d _
pm5.32d _