Theorem mtand

A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypotheses
mtand.1
\( \vdash \varphi \rightarrow \neg \chi \)
mtand.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
l0
mtand.1
\( \vdash \varphi \rightarrow \neg \chi \)
mtand.2
ex _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mtod l0 _