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  4352  phpm  6868  diffisn  6896  tridc  6902  nnnninfeq  7129  pm54.43  7192  addcanprleml  7616  addcanprlemu  7617  iseqf1olemklt  10488  isprm5lem  12144  pw2dvdseulemle  12170  sqne2sq  12180  pythagtriplem4  12271  pythagtriplem11  12277  pythagtriplem13  12279  ctinfomlemom  12431  lssvancl1  13465  ivthinc  14282  pwle2  14910