Theorem mtod 201

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mtoi  202  mtbid  327  mtbird  328  mtand  828  mtord  893  nrmod  3842  po2nr  5581  po3nr  5582  ordn2lp  6381  ordnbtwn  6457  fpropnf1  7268  tfi  7853  nnlim  7880  frrlem14  8302  smoord  8358  tz7.48-3  8437  oalimcl  8551  omlimcl  8569  oneo  8572  omopth2  8575  nnneo  8647  mapdom2  9150  sucdom2  9201  php2  9206  1sdom2dom  9228  isfinite2  9272  domunfican  9295  ordtypelem7  9500  unxpwdom2  9564  cantnfp1lem2  9662  oemapvali  9667  cantnflem1  9672  cantnflem2  9673  rankpwi  9809  tskwe  9959  alephordi  10081  alephdom  10088  cardaleph  10096  cflim2  10269  isfin4p1  10321  fin23lem26  10331  fin1a2lem13  10418  axcclem  10463  fpwwe2lem11  10654  fpwwe2lem12  10655  fpwwe2  10656  pwxpndom2  10678  pwxpndom  10679  pwdjundom  10680  gchaleph  10684  r1wunlim  10750  inatsk  10791  tskuni  10796  gruina  10831  prlem934  11046  dedekind  11401  prodge0rd  13155  qextltlem  13258  ixxub  13423  ixxlb  13424  seqf1olem1  14109  facndiv  14356  cnpart  15331  rlimuni  15641  rlimcld2  15669  isercoll  15759  incexclem  15929  isumltss  15941  alzdvds  16416  fzm1ndvds  16418  fzo0dvdseq  16419  bitsfzolem  16530  smuval2  16578  smupvallem  16579  bezoutlem3  16637  rpdvds  16756  nonsq  16856  prmdiv  16882  odzdvds  16893  pcprendvds  16938  pcprendvds2  16939  pcpremul  16941  pcdvdsb  16967  pcadd2  16988  pockthlem  17003  prmreclem5  17018  prmreclem6  17019  1arith  17025  4sqlem11  17053  vdwlem11  17089  vdwlem12  17090  ramubcl  17116  mrissmrcd  17734  pltnlt  18432  acsfiindd  18647  odcl2  19698  gexnnod  19721  pgpssslw  19747  torsubg  19987  lt6abl  20028  ablfacrplem  20200  pgpfac1lem3  20212  ablsimpnosubgd  20239  irredrmul  20574  islbs3  21348  lbsextlem3  21353  lbsextlem4  21354  f1lindf  22041  mvrf1  22206  psdmul  22400  perfopn  23416  pnfnei  23451  mnfnei  23452  haust1  23583  cmpcld  23633  ptbasfi  23813  fbncp  24071  isfild  24090  fbasfip  24100  filufint  24152  rnelfmlem  24184  fmfnfm  24190  fclscf  24257  ptcmplem3  24286  opnsubg  24340  bldisj  24630  iccntr  25054  icccmplem2  25056  reconnlem1  25059  reconnlem2  25060  evth  25193  lebnumlem3  25197  ovolicc2lem3  25753  volfiniun  25781  iundisj  25782  dvne0  26245  lhop2  26249  itgsubstlem  26282  coemullem  26483  rnplynfin  26546  plyexmo  26552  logccne0  26823  rtprmirr  27005  lgamgulmlem1  27273  wilthlem2  27313  wilth  27315  mumul  27425  chtublem  27455  perfect1  27472  lgsdilem2  27577  lgsne0  27579  lgsqrlem2  27591  lgseisenlem1  27619  lgseisenlem2  27620  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  lgsquad2lem1  27628  2sqblem  27675  chebbnd1lem1  27713  pntpbnd2  27831  pntlem3  27853  ostth  27883  ltsval2  27900  nolt02o  27939  nosupbnd1lem2  27953  nosupbnd1  27958  nosupbnd2  27960  noinfbnd1lem2  27968  noinfbnd1  27973  noinfbnd2  27975  noetasuplem4  27980  noetainflem4  27984  cutbdaybnd2lim  28070  oniso  28544  bdayfinbndlem1  28740  z12bdaylem1  28743  umgrnloop0  29574  usgrnloop0ALT  29673  wlkp1lem2  30140  pthdlem2lem  30240  chirredlem1  32879  iundisjf  33070  ofpreima2  33147  iundisjfi  33275  rprmndvdsru  33947  antnest  36276  antnestlaw3lem  36277  fundmpss  36354  dfon2lem4  36371  dfon2lem7  36374  broutsideof2  36710  outsidele  36720  nn0prpwlem  36949  onint1  37076  fin2so  38369  lindsadd  38375  suceldisj  39574  lpssat  39894  exatleN  40285  3noncolr2  40330  4noncolr3  40334  3dimlem3  40342  3dimlem3OLDN  40343  3dimlem4a  40344  3dimlem4  40345  3dimlem4OLDN  40346  3atlem4  40367  3atlem5  40368  3atlem6  40369  llnnleat  40394  lplnnle2at  40422  lvolnle3at  40463  4atlem0a  40474  4atlem0ae  40475  dalem21  40575  dalem54  40607  cdlemblem  40674  lhpmcvr4N  40907  4atexlemnclw  40951  cdlemd3  41081  cdleme3g  41115  cdleme3h  41116  cdleme7aa  41123  cdleme7d  41127  cdleme7ga  41129  cdleme11c  41142  cdleme15b  41156  cdleme20zN  41182  cdleme21b  41207  cdleme21c  41208  cdleme21ct  41210  cdleme22b  41222  cdleme32b  41323  cdleme35fnpq  41330  cdleme35f  41335  cdleme36a  41341  cdleme42c  41353  cdleme48bw  41383  cdlemf1  41442  cdlemg2fv2  41481  cdlemg7fvbwN  41488  cdlemg4  41498  cdlemg6c  41501  cdlemg27a  41573  cdlemg27b  41577  cdlemk3  41714  dia2dimlem1  41945  dihord6apre  42137  dihord6b  42141  dihord5apre  42143  dihglbcpreN  42181  dihmeetlem6  42190  dochnel2  42273  dochexmidlem7  42347  lspindp5  42651  mapdh8b  42661  hdmapip0  42796  aks6d1c2p2  42993  flt4lem5elem  43505  flt4lem7  43513  nna4b4nsq  43514  pellexlem6  43683  elpell14qr2  43711  pellfundglb  43734  jm2.19  43842  jm2.26lem3  43850  setindtr  43873  harinf  43883  dgraa0p  43998  tfsconcatb0  44193  gneispace0nelrn3  44990  nellindf  50811