Theorem mtand 671

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 115	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 669	1 ⊢ (𝜑 → ¬ 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem is referenced by:  frirrg  4449  phpm  7057  diffisn  7087  tridc  7094  nnnninfeq  7332  pm54.43  7400  addcanprleml  7839  addcanprlemu  7840  iseqf1olemklt  10766  isprm5lem  12736  pw2dvdseulemle  12762  sqne2sq  12772  pythagtriplem4  12864  pythagtriplem11  12870  pythagtriplem13  12872  ctinfomlemom  13071  rrgnz  14306  lssvancl1  14405  ivthinc  15396  g0wlk0  16250  pwle2  16659  nninfnfiinf  16688