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  4447  phpm  7052  diffisn  7082  tridc  7089  nnnninfeq  7327  pm54.43  7395  addcanprleml  7834  addcanprlemu  7835  iseqf1olemklt  10761  isprm5lem  12715  pw2dvdseulemle  12741  sqne2sq  12751  pythagtriplem4  12843  pythagtriplem11  12849  pythagtriplem13  12851  ctinfomlemom  13050  rrgnz  14285  lssvancl1  14384  ivthinc  15370  g0wlk0  16224  pwle2  16620  nninfnfiinf  16646