Theorem mtand 665

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 663	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 614  ax-in2 615

This theorem is referenced by:  frirrg  4348  phpm  6860  diffisn  6888  tridc  6894  nnnninfeq  7121  pm54.43  7184  addcanprleml  7608  addcanprlemu  7609  iseqf1olemklt  10478  isprm5lem  12131  pw2dvdseulemle  12157  sqne2sq  12167  pythagtriplem4  12258  pythagtriplem11  12264  pythagtriplem13  12266  ctinfomlemom  12418  ivthinc  13903  pwle2  14519