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  4418  phpm  6995  diffisn  7023  tridc  7029  nnnninfeq  7263  pm54.43  7331  addcanprleml  7769  addcanprlemu  7770  iseqf1olemklt  10687  isprm5lem  12629  pw2dvdseulemle  12655  sqne2sq  12665  pythagtriplem4  12757  pythagtriplem11  12763  pythagtriplem13  12765  ctinfomlemom  12964  rrgnz  14197  lssvancl1  14296  ivthinc  15282  pwle2  16275  nninfnfiinf  16300