Theorem intn3an1d

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 (\psi \wedge \chi \wedge \theta) \)
Proof
l0
intn3and.1
\( \vdash \varphi \rightarrow \neg \psi \)
simp1
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \psi \)
nsyl l0 _