Theorem anbi1d

Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

anbid.1

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

Conclusion

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

Proof

anbid.1

a1d _

pm5.32rd _