Theorem mtand 669

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 667	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 617  ax-in2 618

This theorem is referenced by:  frirrg  4445  phpm  7047  diffisn  7077  tridc  7084  nnnninfeq  7321  pm54.43  7389  addcanprleml  7827  addcanprlemu  7828  iseqf1olemklt  10753  isprm5lem  12706  pw2dvdseulemle  12732  sqne2sq  12742  pythagtriplem4  12834  pythagtriplem11  12840  pythagtriplem13  12842  ctinfomlemom  13041  rrgnz  14275  lssvancl1  14374  ivthinc  15360  g0wlk0  16181  pwle2  16549  nninfnfiinf  16575