Theorem anbi2i

Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

anbi.1

\( \vdash \varphi \leftrightarrow \psi \)

Conclusion

\( \vdash \chi \wedge \varphi \leftrightarrow \chi \wedge \psi \)

Proof

anbi.1

a1i _

pm5.32i _