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  4283  po2nr  4400  po3nr  4401  sotricim  4414  elirr  4633  ordn2lp  4637  en2lp  4646  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  nndomo  7033  fnfi  7111  difinfsnlem  7274  nninfwlpoimlemginf  7351  2omotaplemap  7451  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprlemladdrl  7873  caucvgprprlemaddq  7903  msqge0  8771  mulge0  8774  squeeze0  9059  elnn0z  9467  fznlem  10245  frec2uzf1od  10636  seqf1oglem1  10749  facndiv  10969  sumrbdclem  11896  prodrbdclem  12090  alzdvds  12373  fzm1ndvds  12375  fzo0dvdseq  12376  bitsfzolem  12473  bitsfzo  12474  rpdvds  12629  nonsq  12737  prmdiv  12765  odzdvds  12776  pcprendvds  12821  pcprendvds2  12822  pcpremul  12824  pcdvdsb  12851  pcadd2  12872  pockthlem  12887  1arith  12898  4sqlem11  12932  4sqlem17  12938  ennnfonelemim  13003  bldisj  15083  perfect1  15680  lgsdilem2  15723  lgsne0  15725  lgseisenlem1  15757  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem1  15768  umgrnloop0  15925  bj-nnen2lp  16341  pwtrufal  16392  refeq  16426