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  825  mtord  890  po2nr  5567  po3nr  5568  ordn2lp  6362  ordnbtwn  6437  fpropnf1  7247  tfi  7829  nnlim  7856  frrlem14  8275  smoord  8331  tz7.48-3  8410  oalimcl  8524  omlimcl  8542  oneo  8545  omopth2  8548  nnneo  8620  mapdom2  9116  sucdom2  9167  php2  9172  1sdom2dom  9194  isfinite2  9238  domunfican  9262  ordtypelem7  9469  unxpwdom2  9533  cantnfp1lem2  9631  oemapvali  9636  cantnflem1  9641  cantnflem2  9642  rankpwi  9778  tskwe  9905  alephordi  10027  alephdom  10034  cardaleph  10042  cflim2  10217  isfin4p1  10269  fin23lem26  10279  fin1a2lem13  10366  axcclem  10411  fpwwe2lem11  10596  fpwwe2lem12  10597  fpwwe2  10598  pwxpndom2  10620  pwxpndom  10621  pwdjundom  10622  gchaleph  10626  r1wunlim  10692  inatsk  10733  tskuni  10738  gruina  10773  prlem934  10988  dedekind  11343  prodge0rd  13099  qextltlem  13202  ixxub  13367  ixxlb  13368  seqf1olem1  14051  facndiv  14298  cnpart  15250  rlimuni  15560  rlimcld2  15588  isercoll  15678  incexclem  15849  isumltss  15861  alzdvds  16337  fzm1ndvds  16339  fzo0dvdseq  16340  bitsfzolem  16451  smuval2  16499  smupvallem  16500  bezoutlem3  16558  rpdvds  16677  nonsq  16777  prmdiv  16803  odzdvds  16814  pcprendvds  16859  pcprendvds2  16860  pcpremul  16862  pcdvdsb  16888  pcadd2  16909  pockthlem  16924  prmreclem5  16939  prmreclem6  16940  1arith  16946  4sqlem11  16974  vdwlem11  17010  vdwlem12  17011  ramubcl  17037  mrissmrcd  17655  pltnlt  18353  acsfiindd  18568  odcl2  19588  gexnnod  19611  pgpssslw  19637  torsubg  19877  lt6abl  19918  ablfacrplem  20090  pgpfac1lem3  20102  ablsimpnosubgd  20129  irredrmul  20455  islbs3  21205  lbsextlem3  21210  lbsextlem4  21211  f1lindf  21854  mvrf1  22017  psdmul  22211  perfopn  23225  pnfnei  23260  mnfnei  23261  haust1  23392  cmpcld  23442  ptbasfi  23621  fbncp  23879  isfild  23898  fbasfip  23908  filufint  23960  rnelfmlem  23992  fmfnfm  23998  fclscf  24065  ptcmplem3  24094  opnsubg  24148  bldisj  24438  iccntr  24862  icccmplem2  24864  reconnlem1  24867  reconnlem2  24868  evth  25001  lebnumlem3  25005  ovolicc2lem3  25561  volfiniun  25589  iundisj  25590  dvne0  26053  lhop2  26057  itgsubstlem  26090  coemullem  26290  plyexmo  26354  logccne0  26620  rtprmirr  26802  lgamgulmlem1  27070  wilthlem2  27110  wilth  27112  mumul  27222  chtublem  27252  perfect1  27269  lgsdilem2  27374  lgsne0  27376  lgsqrlem2  27388  lgseisenlem1  27416  lgseisenlem2  27417  lgsquadlem1  27421  lgsquadlem2  27422  lgsquadlem3  27423  lgsquad2lem1  27425  2sqblem  27472  chebbnd1lem1  27510  pntpbnd2  27628  pntlem3  27650  ostth  27680  ltsval2  27697  nolt02o  27736  nosupbnd1lem2  27750  nosupbnd1  27755  nosupbnd2  27757  noinfbnd1lem2  27765  noinfbnd1  27770  noinfbnd2  27772  noetasuplem4  27777  noetainflem4  27781  cutbdaybnd2lim  27867  oniso  28341  bdayfinbndlem1  28537  z12bdaylem1  28540  umgrnloop0  29256  usgrnloop0ALT  29352  wlkp1lem2  29819  pthdlem2lem  29913  chirredlem1  32539  iundisjf  32738  ofpreima2  32818  iundisjfi  32948  rprmndvdsru  33686  antnest  36003  antnestlaw3lem  36004  fundmpss  36081  dfon2lem4  36098  dfon2lem7  36101  broutsideof2  36436  outsidele  36446  nn0prpwlem  36646  onint1  36773  fin2so  38070  lindsadd  38076  suceldisj  39281  lpssat  39601  exatleN  39992  3noncolr2  40037  4noncolr3  40041  3dimlem3  40049  3dimlem3OLDN  40050  3dimlem4a  40051  3dimlem4  40052  3dimlem4OLDN  40053  3atlem4  40074  3atlem5  40075  3atlem6  40076  llnnleat  40101  lplnnle2at  40129  lvolnle3at  40170  4atlem0a  40181  4atlem0ae  40182  dalem21  40282  dalem54  40314  cdlemblem  40381  lhpmcvr4N  40614  4atexlemnclw  40658  cdlemd3  40788  cdleme3g  40822  cdleme3h  40823  cdleme7aa  40830  cdleme7d  40834  cdleme7ga  40836  cdleme11c  40849  cdleme15b  40863  cdleme20zN  40889  cdleme21b  40914  cdleme21c  40915  cdleme21ct  40917  cdleme22b  40929  cdleme32b  41030  cdleme35fnpq  41037  cdleme35f  41042  cdleme36a  41048  cdleme42c  41060  cdleme48bw  41090  cdlemf1  41149  cdlemg2fv2  41188  cdlemg7fvbwN  41195  cdlemg4  41205  cdlemg6c  41208  cdlemg27a  41280  cdlemg27b  41284  cdlemk3  41421  dia2dimlem1  41652  dihord6apre  41844  dihord6b  41848  dihord5apre  41850  dihglbcpreN  41888  dihmeetlem6  41897  dochnel2  41980  dochexmidlem7  42054  lspindp5  42358  mapdh8b  42368  hdmapip0  42503  aks6d1c2p2  42700  flt4lem5elem  43197  flt4lem7  43205  nna4b4nsq  43206  pellexlem6  43375  elpell14qr2  43403  pellfundglb  43426  jm2.19  43534  jm2.26lem3  43542  setindtr  43565  harinf  43575  dgraa0p  43690  tfsconcatb0  43885  gneispace0nelrn3  44682