Theorem nanbi1i

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

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