Theorem mtod 669

Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
mtod.1	⊢ (𝜑 → ¬ 𝜒)
mtod.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mtod	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtod

Step	Hyp	Ref	Expression
1		mtod.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mtod.1	. . 3 ⊢ (𝜑 → ¬ 𝜒)
3	2	a1d 22	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 666	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 619  ax-in2 620

This theorem is referenced by:  mtoi  670  mtand  671  mtbid  678  mtbird  679  pwntru  4291  po2nr  4408  po3nr  4409  sotricim  4422  elirr  4641  ordn2lp  4645  en2lp  4654  tfr1onlemsucaccv  6512  tfrcllemsucaccv  6525  nndomo  7055  fnfi  7140  difinfsnlem  7303  nninfwlpoimlemginf  7380  2omotaplemap  7481  cauappcvgprlemladdru  7881  cauappcvgprlemladdrl  7882  caucvgprlemladdrl  7903  caucvgprprlemaddq  7933  msqge0  8801  mulge0  8804  squeeze0  9089  elnn0z  9497  fznlem  10281  frec2uzf1od  10674  seqf1oglem1  10787  facndiv  11007  sumrbdclem  11961  prodrbdclem  12155  alzdvds  12438  fzm1ndvds  12440  fzo0dvdseq  12441  bitsfzolem  12538  bitsfzo  12539  rpdvds  12694  nonsq  12802  prmdiv  12830  odzdvds  12841  pcprendvds  12886  pcprendvds2  12887  pcpremul  12889  pcdvdsb  12916  pcadd2  12937  pockthlem  12952  1arith  12963  4sqlem11  12997  4sqlem17  13003  ennnfonelemim  13068  bldisj  15154  perfect1  15751  lgsdilem2  15794  lgsne0  15796  lgseisenlem1  15828  lgseisenlem2  15829  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  lgsquad2lem1  15839  umgrnloop0  15997  bj-nnen2lp  16609  pwtrufal  16658  refeq  16695