Theorem mtand 671

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 669	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 619  ax-in2 620

This theorem is referenced by:  frirrg  4473  phpm  7122  diffisn  7152  tridc  7159  nnnninfeq  7421  pm54.43  7489  addcanprleml  7934  addcanprlemu  7935  iseqf1olemklt  10867  sshashneg  11213  isprm5lem  12846  pw2dvdseulemle  12872  sqne2sq  12882  pythagtriplem4  12974  pythagtriplem11  12980  pythagtriplem13  12982  ballotfilemfcc  13158  ctinfomlemom  13199  rrgnz  14437  lssvancl1  14564  ivthinc  15557  g0wlk0  16414  pwle2  16821  nninfnfiinf  16850