Theorem inegd

Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)

Hypothesis
inegd.1
\( \vdash \varphi \wedge \psi \rightarrow \bot \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
inegd.1
l1
ex _
\( \vdash \varphi \rightarrow \psi \rightarrow \bot \)
dfnot
\( \vdash \neg \psi \leftrightarrow \psi \rightarrow \bot \)
sylibr l1 _