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  4284  po2nr  4401  po3nr  4402  sotricim  4415  elirr  4634  ordn2lp  4638  en2lp  4647  tfr1onlemsucaccv  6498  tfrcllemsucaccv  6511  nndomo  7038  fnfi  7119  difinfsnlem  7282  nninfwlpoimlemginf  7359  2omotaplemap  7459  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  caucvgprprlemaddq  7911  msqge0  8779  mulge0  8782  squeeze0  9067  elnn0z  9475  fznlem  10254  frec2uzf1od  10645  seqf1oglem1  10758  facndiv  10978  sumrbdclem  11909  prodrbdclem  12103  alzdvds  12386  fzm1ndvds  12388  fzo0dvdseq  12389  bitsfzolem  12486  bitsfzo  12487  rpdvds  12642  nonsq  12750  prmdiv  12778  odzdvds  12789  pcprendvds  12834  pcprendvds2  12835  pcpremul  12837  pcdvdsb  12864  pcadd2  12885  pockthlem  12900  1arith  12911  4sqlem11  12945  4sqlem17  12951  ennnfonelemim  13016  bldisj  15096  perfect1  15693  lgsdilem2  15736  lgsne0  15738  lgseisenlem1  15770  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2lem1  15781  umgrnloop0  15938  bj-nnen2lp  16426  pwtrufal  16476  refeq  16510