Theorem intnand

Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis
intnand.1
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg (\chi \wedge \psi) \)
Proof
l0
intnand.1
\( \vdash \varphi \rightarrow \neg \psi \)
simpr
\( \vdash \chi \wedge \psi \rightarrow \psi \)
nsyl l0 _