Theorem nanbi2i

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

Hypothesis
nanbii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \chi \barwedge \varphi \leftrightarrow \chi \barwedge \psi \)
Proof
l0
nanbii.1
\( \vdash \varphi \leftrightarrow \psi \)
nanbi2
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\chi \barwedge \varphi \leftrightarrow \chi \barwedge \psi) \)
ax-mp l0 _