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  4470  phpm  7119  diffisn  7149  tridc  7156  nnnninfeq  7418  pm54.43  7486  addcanprleml  7925  addcanprlemu  7926  iseqf1olemklt  10856  sshashneg  11198  isprm5lem  12831  pw2dvdseulemle  12857  sqne2sq  12867  pythagtriplem4  12959  pythagtriplem11  12965  pythagtriplem13  12967  ctinfomlemom  13167  rrgnz  14403  lssvancl1  14502  ivthinc  15495  g0wlk0  16352  pwle2  16759  nninfnfiinf  16788