Theorem intn3an2d

Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypothesis
intn3and.1
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg (\chi \wedge \psi \wedge \theta) \)
Proof
l0
intn3and.1
\( \vdash \varphi \rightarrow \neg \psi \)
simp2
\( \vdash \chi \wedge \psi \wedge \theta \rightarrow \psi \)
nsyl l0 _