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  4386  phpm  6935  diffisn  6963  tridc  6969  nnnninfeq  7203  pm54.43  7271  addcanprleml  7700  addcanprlemu  7701  iseqf1olemklt  10609  isprm5lem  12336  pw2dvdseulemle  12362  sqne2sq  12372  pythagtriplem4  12464  pythagtriplem11  12470  pythagtriplem13  12472  ctinfomlemom  12671  rrgnz  13902  lssvancl1  14001  ivthinc  14965  pwle2  15731  nninfnfiinf  15756