Theorem mtand 660

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

Hypotheses

Ref	Expression
mtand.1	⊢ (𝜑 → ¬ 𝜒)
mtand.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mtand	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtand

Step	Hyp	Ref	Expression
1		mtand.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mtand.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 114	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 658	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem is referenced by:  frirrg  4335  phpm  6843  diffisn  6871  tridc  6877  nnnninfeq  7104  pm54.43  7167  addcanprleml  7576  addcanprlemu  7577  iseqf1olemklt  10441  isprm5lem  12095  pw2dvdseulemle  12121  sqne2sq  12131  pythagtriplem4  12222  pythagtriplem11  12228  pythagtriplem13  12230  ctinfomlemom  12382  ivthinc  13415  pwle2  14031