Theorem mtand 666

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 664	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  4385  phpm  6926  diffisn  6954  tridc  6960  nnnninfeq  7194  pm54.43  7257  addcanprleml  7681  addcanprlemu  7682  iseqf1olemklt  10590  isprm5lem  12309  pw2dvdseulemle  12335  sqne2sq  12345  pythagtriplem4  12437  pythagtriplem11  12443  pythagtriplem13  12445  ctinfomlemom  12644  rrgnz  13824  lssvancl1  13923  ivthinc  14879  pwle2  15643