Theorem anbi1i

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

Hypothesis

anbi.1

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

Conclusion

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

Proof

anbi.1

a1i _

pm5.32ri _