Theorem
imnan
Express an implication in terms of a negated conjunction. (Contributed by NM, 9-Apr-1994.)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
Proof
df-an
con2bii
_
This is the content in the right pane.