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  4476  phpm  7133  diffisn  7163  tridc  7170  nnnninfeq  7432  pm54.43  7500  addcanprleml  7945  addcanprlemu  7946  iseqf1olemklt  10887  sshashneg  11233  isprm5lem  12866  pw2dvdseulemle  12892  sqne2sq  12902  pythagtriplem4  12994  pythagtriplem11  13000  pythagtriplem13  13002  ballotfilemfcc  13180  ballotfilemi1  13192  ballotfilemii  13193  ctinfomlemom  13265  rrgnz  14518  lssvancl1  14644  ivthinc  15637  g0wlk0  16494  pwle2  16911  nninfnfiinf  16940