Theorem mtand 675

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 673	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem is used by:  frirrg  4497  phpm  7172  diffisn  7202  tridc  7209  nnnninfeq  7475  pm54.43  7543  addcanprleml  7988  addcanprlemu  7989  iseqf1olemklt  10957  sshashneg  11304  isprm5lem  12946  pwbdvdseulemle  12972  sqne2sq  12983  pythagtriplem4  13077  pythagtriplem11  13083  pythagtriplem13  13085  ballotfilemfcc  13292  ballotfilemi1  13304  ballotfilemii  13305  ctinfomlemom  13377  rrgnz  14687  lssvancl1  14814  ivthinc  15881  g0wlk0  16828  pwle2  17245  nninfnfiinf  17284