Theorem nanbi1

Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\varphi \barwedge \chi \leftrightarrow \psi \barwedge \chi) \)
Proof
l0
imbi1
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\varphi \rightarrow \neg \chi \leftrightarrow \psi \rightarrow \neg \chi) \)
l1
dfnan2
\( \vdash \varphi \barwedge \chi \leftrightarrow \varphi \rightarrow \neg \chi \)
dfnan2
\( \vdash \psi \barwedge \chi \leftrightarrow \psi \rightarrow \neg \chi \)
3bitr4g l0 l1 _