Theorem nanbi2

Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011.) (Proof shortened by SF, 2-Jan-2018.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\chi \barwedge \varphi \leftrightarrow \chi \barwedge \psi) \)
Proof
l0
nanbi1
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\varphi \barwedge \chi \leftrightarrow \psi \barwedge \chi) \)
l1
nancom
\( \vdash \chi \barwedge \varphi \leftrightarrow \varphi \barwedge \chi \)
nancom
\( \vdash \chi \barwedge \psi \leftrightarrow \psi \barwedge \chi \)
3bitr4g l0 l1 _