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  4381  phpm  6921  diffisn  6949  tridc  6955  nnnninfeq  7187  pm54.43  7250  addcanprleml  7674  addcanprlemu  7675  iseqf1olemklt  10569  isprm5lem  12279  pw2dvdseulemle  12305  sqne2sq  12315  pythagtriplem4  12406  pythagtriplem11  12412  pythagtriplem13  12414  ctinfomlemom  12584  rrgnz  13764  lssvancl1  13863  ivthinc  14797  pwle2  15489