Theorem
anbi2
Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.)
Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\chi \wedge \varphi \leftrightarrow \chi \wedge \psi) \)
Proof
id
anbi2d
_
This is the content in the right pane.