Theorem mtand

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

	Ref	Expression
Hypotheses	mtand.1	$$⊢\phi \to \neg \chi$$
	mtand.2	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
Assertion	mtand	$$⊢\phi \to \neg \psi$$

Proof

Step	Hyp	Ref	Expression
1		mtand.1	$$⊢\phi \to \neg \chi$$
2		mtand.2	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
3	2	ex	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	1 3	mtod	$$⊢\phi \to \neg \psi$$