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

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 623  ax-in2 624

This theorem is referenced by:  frirrg  4493  phpm  7161  diffisn  7191  tridc  7198  nnnninfeq  7462  pm54.43  7530  addcanprleml  7975  addcanprlemu  7976  iseqf1olemklt  10918  sshashneg  11264  isprm5lem  12902  pw2dvdseulemle  12928  sqne2sq  12938  pythagtriplem4  13030  pythagtriplem11  13036  pythagtriplem13  13038  ballotfilemfcc  13216  ballotfilemi1  13228  ballotfilemii  13229  ctinfomlemom  13301  rrgnz  14560  lssvancl1  14687  ivthinc  15727  g0wlk0  16594  pwle2  17011  nninfnfiinf  17040