Theorem imnani

Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)

Hypothesis
imnani.1
\( \vdash \neg (\varphi \wedge \psi) \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
l0
imnani.1
\( \vdash \neg (\varphi \wedge \psi) \)
imnan
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
mpbir l0 _