MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtod Unicode version

Theorem mtod 177
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
StepHypRef Expression
1 mtod.2 . 2
2 mtod.1 . . 3
32a1d 25 . 2
41, 3pm2.65d 175 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  mtoi  178  mtbid  300  mtbird  301  mtand  659  mtord  660  po2nr  4818  po3nr  4819  ordn2lp  4903  onssneli  4992  tfi  6688  nnlim  6713  smoord  7055  tz7.48-3  7128  oalimcl  7228  omlimcl  7246  oneo  7249  omopth2  7252  nnneo  7319  mapdom2  7708  php3  7723  onomeneq  7727  sucdom2  7734  isfinite2  7798  domunfican  7813  ordtypelem7  7970  unxpwdom2  8035  cantnfp1lem2  8119  oemapvali  8124  cantnflem1  8129  cantnflem2  8130  cantnfp1lem2OLD  8145  cantnflem1OLD  8152  rankpwi  8262  tskwe  8352  alephordi  8476  alephdom  8483  cardaleph  8491  cflim2  8664  isfin4-3  8716  fin23lem26  8726  fin1a2lem13  8813  axcclem  8858  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  pwxpndom2  9064  pwxpndom  9065  pwcdandom  9066  gchaleph  9070  r1wunlim  9136  inatsk  9177  tskuni  9182  gruina  9217  prlem934  9432  dedekind  9765  qextltlem  11430  ixxub  11579  ixxlb  11580  seqf1olem1  12146  facndiv  12366  cnpart  13073  rlimuni  13373  rlimcld2  13401  isercoll  13490  incexclem  13648  isumltss  13660  alzdvds  14036  fzm1ndvds  14038  fzo0dvdseq  14039  bitsfzolem  14084  smuval2  14132  smupvallem  14133  bezoutlem3  14178  rpdvds  14265  nonsq  14292  prmdiv  14315  odzdvds  14322  pcprendvds  14364  pcprendvds2  14365  pcpremul  14367  pcdvdsb  14392  pcadd2  14409  pockthlem  14423  prmreclem5  14438  prmreclem6  14439  1arith  14445  4sqlem11  14473  vdwlem11  14509  vdwlem12  14510  ramubcl  14536  mrissmrcd  15037  pltnlt  15598  acsfiindd  15807  odcl2  16587  gexnnod  16608  pgpssslw  16634  torsubg  16860  lt6abl  16897  ablfacrplem  17116  pgpfac1lem3  17128  irredrmul  17356  islbs3  17801  lbsextlem3  17806  lbsextlem4  17807  rng1nfld  17926  mvrf1  18081  f1lindf  18857  perfopn  19686  pnfnei  19721  mnfnei  19722  haust1  19853  cmpcld  19902  ptbasfi  20082  fbncp  20340  isfild  20359  fbasfip  20369  filufint  20421  rnelfmlem  20453  fmfnfm  20459  fclscf  20526  ptcmplem3  20554  opnsubg  20606  bldisj  20901  iccntr  21326  icccmplem2  21328  reconnlem1  21331  reconnlem2  21332  evth  21459  lebnumlem3  21463  ovolicc2lem3  21930  volfiniun  21957  iundisj  21958  dvne0  22412  lhop2  22416  itgsubstlem  22449  coemullem  22647  plyexmo  22709  wilthlem2  23343  wilth  23345  mumul  23455  chtublem  23486  perfect1  23503  lgsdilem2  23606  lgsne0  23608  lgsqrlem2  23617  lgseisenlem1  23624  lgseisenlem2  23625  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  lgsquad2lem1  23633  2sqblem  23652  chebbnd1lem1  23654  pntpbnd2  23772  pntlem3  23794  ostth  23824  vdgr1a  24906  chirredlem1  27309  iundisjf  27448  ofpreima2  27508  iundisjfi  27601  logccne0  28012  lgamgulmlem1  28571  fundmpss  29196  dfon2lem4  29218  dfon2lem7  29221  sltval2  29416  sltasym  29432  broutsideof2  29772  outsidele  29782  onint1  29914  fin2so  30040  nn0prpwlem  30140  nn0prpw  30141  pellexlem6  30770  elpell14qr2  30798  pellfundglb  30821  jm2.19  30935  jm2.26lem3  30943  setindtr  30966  harinf  30976  dgraa0p  31098  lpssat  34738  exatleN  35128  3noncolr2  35173  4noncolr3  35177  3dimlem3  35185  3dimlem3OLDN  35186  3dimlem4a  35187  3dimlem4  35188  3dimlem4OLDN  35189  3atlem4  35210  3atlem5  35211  3atlem6  35212  llnnleat  35237  lplnnle2at  35265  lvolnle3at  35306  4atlem0a  35317  4atlem0ae  35318  dalem21  35418  dalem54  35450  cdlemblem  35517  lhpmcvr4N  35750  4atexlemnclw  35794  cdlemd3  35925  cdleme3g  35959  cdleme3h  35960  cdleme7aa  35967  cdleme7d  35971  cdleme7ga  35973  cdleme11c  35986  cdleme15b  36000  cdleme20zN  36026  cdleme20yOLD  36028  cdleme21b  36052  cdleme21c  36053  cdleme21ct  36055  cdleme22b  36067  cdleme32b  36168  cdleme35fnpq  36175  cdleme35f  36180  cdleme36a  36186  cdleme42c  36198  cdleme48bw  36228  cdlemf1  36287  cdlemg2fv2  36326  cdlemg7fvbwN  36333  cdlemg4  36343  cdlemg6c  36346  cdlemg27a  36418  cdlemg27b  36422  cdlemk3  36559  dia2dimlem1  36791  dihord6apre  36983  dihord6b  36987  dihord5apre  36989  dihglbcpreN  37027  dihmeetlem6  37036  dochnel2  37119  dochexmidlem7  37193  lspindp5  37497  mapdh8b  37507  hdmapip0  37645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator