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  4442  phpm  7040  diffisn  7068  tridc  7075  nnnninfeq  7311  pm54.43  7379  addcanprleml  7817  addcanprlemu  7818  iseqf1olemklt  10737  isprm5lem  12684  pw2dvdseulemle  12710  sqne2sq  12720  pythagtriplem4  12812  pythagtriplem11  12818  pythagtriplem13  12820  ctinfomlemom  13019  rrgnz  14253  lssvancl1  14352  ivthinc  15338  g0wlk0  16142  pwle2  16477  nninfnfiinf  16503