Theorem mtand 669

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 667	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 617  ax-in2 618

This theorem is referenced by:  frirrg  4441  phpm  7035  diffisn  7063  tridc  7069  nnnninfeq  7303  pm54.43  7371  addcanprleml  7809  addcanprlemu  7810  iseqf1olemklt  10728  isprm5lem  12671  pw2dvdseulemle  12697  sqne2sq  12707  pythagtriplem4  12799  pythagtriplem11  12805  pythagtriplem13  12807  ctinfomlemom  13006  rrgnz  14240  lssvancl1  14339  ivthinc  15325  g0wlk0  16091  pwle2  16393  nninfnfiinf  16419