Theorem mtand 655

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 114	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 653	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem is referenced by:  frirrg  4328  phpm  6831  diffisn  6859  tridc  6865  nnnninfeq  7092  pm54.43  7146  addcanprleml  7555  addcanprlemu  7556  iseqf1olemklt  10420  isprm5lem  12073  pw2dvdseulemle  12099  sqne2sq  12109  pythagtriplem4  12200  pythagtriplem11  12206  pythagtriplem13  12208  ctinfomlemom  12360  ivthinc  13261  pwle2  13878