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  4495  phpm  7167  diffisn  7197  tridc  7204  nnnninfeq  7468  pm54.43  7536  addcanprleml  7981  addcanprlemu  7982  iseqf1olemklt  10937  sshashneg  11283  isprm5lem  12921  pw2dvdseulemle  12947  sqne2sq  12957  pythagtriplem4  13049  pythagtriplem11  13055  pythagtriplem13  13057  ballotfilemfcc  13235  ballotfilemi1  13247  ballotfilemii  13248  ctinfomlemom  13320  rrgnz  14579  lssvancl1  14706  ivthinc  15746  g0wlk0  16623  pwle2  17040  nninfnfiinf  17078