Theorem mtod 667

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 664	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  668  mtand  669  mtbid  676  mtbird  677  pwntru  4262  po2nr  4377  po3nr  4378  sotricim  4391  elirr  4610  ordn2lp  4614  en2lp  4623  tfr1onlemsucaccv  6457  tfrcllemsucaccv  6470  nndomo  6993  fnfi  7071  difinfsnlem  7234  nninfwlpoimlemginf  7311  2omotaplemap  7411  cauappcvgprlemladdru  7811  cauappcvgprlemladdrl  7812  caucvgprlemladdrl  7833  caucvgprprlemaddq  7863  msqge0  8731  mulge0  8734  squeeze0  9019  elnn0z  9427  fznlem  10205  frec2uzf1od  10595  seqf1oglem1  10708  facndiv  10928  sumrbdclem  11854  prodrbdclem  12048  alzdvds  12331  fzm1ndvds  12333  fzo0dvdseq  12334  bitsfzolem  12431  bitsfzo  12432  rpdvds  12587  nonsq  12695  prmdiv  12723  odzdvds  12734  pcprendvds  12779  pcprendvds2  12780  pcpremul  12782  pcdvdsb  12809  pcadd2  12830  pockthlem  12845  1arith  12856  4sqlem11  12890  4sqlem17  12896  ennnfonelemim  12961  bldisj  15040  perfect1  15637  lgsdilem2  15680  lgsne0  15682  lgseisenlem1  15714  lgseisenlem2  15715  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2lem1  15725  umgrnloop0  15882  bj-nnen2lp  16227  pwtrufal  16274  refeq  16307