Theorem mtand 667

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 665	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 615  ax-in2 616

This theorem is referenced by:  frirrg  4401  phpm  6969  diffisn  6997  tridc  7003  nnnninfeq  7237  pm54.43  7305  addcanprleml  7734  addcanprlemu  7735  iseqf1olemklt  10650  isprm5lem  12507  pw2dvdseulemle  12533  sqne2sq  12543  pythagtriplem4  12635  pythagtriplem11  12641  pythagtriplem13  12643  ctinfomlemom  12842  rrgnz  14074  lssvancl1  14173  ivthinc  15159  pwle2  16009  nninfnfiinf  16034