Theorem intnan

Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)

Hypothesis
intnan.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \neg (\psi \wedge \varphi) \)
Proof
l0
intnan.1
\( \vdash \neg \varphi \)
simpr
\( \vdash \psi \wedge \varphi \rightarrow \varphi \)
mto l0 _