Theorem nanbi1d

Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)

Hypothesis
nanbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \barwedge \theta \leftrightarrow \chi \barwedge \theta) \)
Proof
l0
nanbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
nanbi1
\( \vdash (\psi \leftrightarrow \chi) \rightarrow (\psi \barwedge \theta \leftrightarrow \chi \barwedge \theta) \)
syl l0 _