Theorem mtod 200

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 25	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 198	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  mtoi  201  mtbid  326  mtbird  327  mtand  814  mtord  876  po2nr  5487  po3nr  5488  ordn2lp  6211  ordnbtwn  6281  fpropnf1  7025  tfi  7568  nnlim  7593  smoord  8002  tz7.48-3  8080  oalimcl  8186  omlimcl  8204  oneo  8207  omopth2  8210  nnneo  8278  mapdom2  8688  php3  8703  onomeneq  8708  sucdom2  8714  isfinite2  8776  domunfican  8791  ordtypelem7  8988  unxpwdom2  9052  cantnfp1lem2  9142  oemapvali  9147  cantnflem1  9152  cantnflem2  9153  rankpwi  9252  tskwe  9379  alephordi  9500  alephdom  9507  cardaleph  9515  cflim2  9685  isfin4p1  9737  fin23lem26  9747  fin1a2lem13  9834  axcclem  9879  fpwwe2lem12  10063  fpwwe2lem13  10064  fpwwe2  10065  pwxpndom2  10087  pwxpndom  10088  pwdjundom  10089  gchaleph  10093  r1wunlim  10159  inatsk  10200  tskuni  10205  gruina  10240  prlem934  10455  dedekind  10803  prodge0rd  12497  qextltlem  12596  ixxub  12760  ixxlb  12761  seqf1olem1  13410  facndiv  13649  cnpart  14599  rlimuni  14907  rlimcld2  14935  isercoll  15024  incexclem  15191  isumltss  15203  alzdvds  15670  fzm1ndvds  15672  fzo0dvdseq  15673  bitsfzolem  15783  smuval2  15831  smupvallem  15832  bezoutlem3  15889  rpdvds  16004  nonsq  16099  prmdiv  16122  odzdvds  16132  pcprendvds  16177  pcprendvds2  16178  pcpremul  16180  pcdvdsb  16205  pcadd2  16226  pockthlem  16241  prmreclem5  16256  prmreclem6  16257  1arith  16263  4sqlem11  16291  vdwlem11  16327  vdwlem12  16328  ramubcl  16354  mrissmrcd  16911  pltnlt  17578  acsfiindd  17787  odcl2  18692  gexnnod  18713  pgpssslw  18739  torsubg  18974  lt6abl  19015  ablfacrplem  19187  pgpfac1lem3  19199  ablsimpnosubgd  19226  irredrmul  19457  islbs3  19927  lbsextlem3  19932  lbsextlem4  19933  rng1nfld  20051  mvrf1  20205  f1lindf  20966  perfopn  21793  pnfnei  21828  mnfnei  21829  haust1  21960  cmpcld  22010  ptbasfi  22189  fbncp  22447  isfild  22466  fbasfip  22476  filufint  22528  rnelfmlem  22560  fmfnfm  22566  fclscf  22633  ptcmplem3  22662  opnsubg  22716  bldisj  23008  iccntr  23429  icccmplem2  23431  reconnlem1  23434  reconnlem2  23435  evth  23563  lebnumlem3  23567  ovolicc2lem3  24120  volfiniun  24148  iundisj  24149  dvne0  24608  lhop2  24612  itgsubstlem  24645  coemullem  24840  plyexmo  24902  logccne0  25162  lgamgulmlem1  25606  wilthlem2  25646  wilth  25648  mumul  25758  chtublem  25787  perfect1  25804  lgsdilem2  25909  lgsne0  25911  lgsqrlem2  25923  lgseisenlem1  25951  lgseisenlem2  25952  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad2lem1  25960  2sqblem  26007  chebbnd1lem1  26045  pntpbnd2  26163  pntlem3  26185  ostth  26215  umgrnloop0  26894  usgrnloop0ALT  26987  wlkp1lem2  27456  pthdlem2lem  27548  chirredlem1  30167  iundisjf  30339  ofpreima2  30411  iundisjfi  30519  fundmpss  33009  dfon2lem4  33031  dfon2lem7  33034  frrlem14  33136  sltval2  33163  nolt02o  33199  nosupbnd1lem2  33209  nosupbnd1  33214  nosupbnd2  33216  noetalem3  33219  broutsideof2  33583  outsidele  33593  nn0prpwlem  33670  onint1  33797  fin2so  34894  lindsadd  34900  poimirlem16  34923  lpssat  36164  exatleN  36555  3noncolr2  36600  4noncolr3  36604  3dimlem3  36612  3dimlem3OLDN  36613  3dimlem4a  36614  3dimlem4  36615  3dimlem4OLDN  36616  3atlem4  36637  3atlem5  36638  3atlem6  36639  llnnleat  36664  lplnnle2at  36692  lvolnle3at  36733  4atlem0a  36744  4atlem0ae  36745  dalem21  36845  dalem54  36877  cdlemblem  36944  lhpmcvr4N  37177  4atexlemnclw  37221  cdlemd3  37351  cdleme3g  37385  cdleme3h  37386  cdleme7aa  37393  cdleme7d  37397  cdleme7ga  37399  cdleme11c  37412  cdleme15b  37426  cdleme20zN  37452  cdleme21b  37477  cdleme21c  37478  cdleme21ct  37480  cdleme22b  37492  cdleme32b  37593  cdleme35fnpq  37600  cdleme35f  37605  cdleme36a  37611  cdleme42c  37623  cdleme48bw  37653  cdlemf1  37712  cdlemg2fv2  37751  cdlemg7fvbwN  37758  cdlemg4  37768  cdlemg6c  37771  cdlemg27a  37843  cdlemg27b  37847  cdlemk3  37984  dia2dimlem1  38215  dihord6apre  38407  dihord6b  38411  dihord5apre  38413  dihglbcpreN  38451  dihmeetlem6  38460  dochnel2  38543  dochexmidlem7  38617  lspindp5  38921  mapdh8b  38931  hdmapip0  39066  rtprmirr  39243  pellexlem6  39480  elpell14qr2  39508  pellfundglb  39531  jm2.19  39639  jm2.26lem3  39647  setindtr  39670  harinf  39680  dgraa0p  39798  gneispace0nelrn3  40541