Theorem annotanannot

A conjunction with a negated conjunction. (Contributed by AV, 8-Mar-2022.) (Proof shortened by Wolf Lammen, 1-Apr-2022.)

Conclusion
\( \vdash \varphi \wedge \neg (\varphi \wedge \psi) \leftrightarrow \varphi \wedge \neg \psi \)
Proof
ibar
bicomd _
notbid _
pm5.32i _