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

Theorem mp1i 12
Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)
Hypotheses
Ref Expression
mp1i.a  |-  ph
mp1i.b  |-  ( ph  ->  ps )
Assertion
Ref Expression
mp1i  |-  ( ch 
->  ps )

Proof of Theorem mp1i
StepHypRef Expression
1 mp1i.a . . 3  |-  ph
2 mp1i.b . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 5 . 2  |-  ps
43a1i 11 1  |-  ( ch 
->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6
This theorem is referenced by:  poirr2  5217  relcoi2  5360  isomin  6023  isoini  6024  supp0  6690  suppval1  6691  suppssr  6715  dmtpos  6752  oaabs2  7076  mapsncnv  7251  boxcutc  7298  domunsncan  7403  pw2f1o  7408  unxpdom2  7513  sucxpdom  7514  findcard2d  7546  ac6sfi  7548  xpfi  7575  imafi  7596  snopfsupp  7635  fifo  7674  ordtypelem4  7727  oismo  7746  wofib  7751  brwdom2  7780  canthwdom  7786  cantnffvalOLD  7863  cantnfval  7868  cantnflt  7872  cantnff  7874  cantnf0  7875  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnflem1b  7886  cantnflem1  7889  cantnfltOLD  7902  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  cantnflem1bOLD  7909  cantnflem1dOLD  7911  cantnflem1OLD  7912  cnfcom  7925  cnfcom2lem  7926  cnfcomOLD  7933  cnfcom2lemOLD  7934  ranksnb  8026  tskwe  8112  cardidm  8121  infxpenc  8176  infxpencOLD  8181  fseqdom  8188  dfac8clem  8194  dfac12lem2  8305  infmap2  8379  isfin4-3  8476  fin23lem14  8494  fin23lem40  8512  isf34lem7  8540  isf34lem6  8541  fin1a2lem12  8572  hsmexlem4  8590  hsmexlem5  8591  ac5b  8639  alephexp1  8735  alephsuc3  8736  axpowndlem2OLD  8755  fpwwe2lem8  8796  fpwwe2lem13  8801  canthwe  8810  canthp1lem2  8812  gchcda1  8815  pwfseqlem5  8822  wunco  8892  prlem934  9194  supsrlem  9270  msqge0  9853  ofnegsub  10312  ofsubge0  10313  xaddpnf1  11188  supxrmnf  11272  injresinjlem  11630  uzindi  11795  seqfeq4  11847  seqof  11855  bcval5  12086  hashdomi  12135  hash1snb  12163  brfi1uzind  12211  lsw0  12259  ccatlen  12267  lswccatn0lsw  12279  s111  12294  swrdspsleq  12334  wrdeqswrdlsw  12335  wrdeqs1cat  12361  reps  12400  repsw0  12407  repswccat  12415  repswrevw  12416  lswcshw  12441  cshwsexa  12450  wrdlen2i  12538  shftfib  12553  limsupcl  12943  limsupgf  12945  limsupval2  12950  isercolllem3  13136  ackbijnn  13283  supcvg  13310  ege2le3  13367  rpnnen2lem5  13493  ruclem11  13514  fsumdvds  13568  bitsinv2  13631  sadaddlem  13654  smupf  13666  smup0  13667  smu01lem  13673  isprm6  13787  hashdvds  13842  reumodprminv  13864  vdwlem13  14046  ramtlecl  14053  0ram  14073  cshwshashnsame  14122  prmlem0  14125  wunndx  14182  prdsval  14385  xpsbas  14504  xpsadd  14506  xpsmul  14507  xpssca  14508  xpsvsca  14509  xpsless  14510  xpsle  14511  mreexexlem2d  14575  mreacs  14588  acsfn  14589  idfu2nd  14779  idfucl  14783  fucsect  14874  setccatid  14944  setcepi  14948  catchomfval  14958  uncfval  15036  oduglb  15301  odumeet  15302  odulub  15303  odujoin  15304  isipodrs  15323  fpwipodrs  15326  isacs4lem  15330  isacs5lem  15331  submacs  15484  frmdup1  15533  mulgneg2  15645  subgacs  15707  nsgacs  15708  idrespermg  15907  psgnunilem5  15991  odf1o2  16063  frgpuplem  16260  cygctb  16359  gsum2dlem2  16450  gsum2dOLD  16452  dprdsubg  16509  dmdprdsplit2lem  16532  dmdprdpr  16536  dprdpr  16537  dpjeq  16546  dpjeqOLD  16553  ablfac1eulem  16561  pgpfac1lem2  16564  pgpfaclem1  16570  srgbinomlem4  16629  unitgrp  16747  isirred  16779  lssacs  17025  pwssplit1  17117  lbsextlem2  17217  lbsextlem3  17218  psrass1lem  17424  psrlidm  17451  psrlidmOLD  17452  resspsradd  17465  resspsrmul  17466  resspsrvsca  17467  ltbwe  17529  psropprmul  17668  coe1add  17693  coe1mul2lem1  17696  coe1tm  17701  evls1rhmlem  17731  evl1sca  17743  evl1var  17745  pf1mpf  17761  pf1ind  17764  xrsmcmn  17814  xrs1mnd  17826  xrs10  17827  gsumfsum  17854  zringlpir  17881  zringcyg  17882  zlpirlem3  17885  zlpir  17886  zcyg  17887  mulgrhmOLD  17904  mulgrhm2OLD  17905  zndvds  17957  regsumsupp  18027  uvcvv1  18189  lsslinds  18235  matmulr  18288  mat0dimbas0  18300  ofco2  18307  mavmul0  18338  mavmul0g  18339  mdetunilem9  18401  maducoeval2  18421  madugsum  18424  smadiadetlem0  18442  smadiadetlem1a  18444  smadiadetlem4  18450  smadiadetglem1  18452  smadiadetglem2  18453  smadiadetg  18454  cramer0  18471  indistopon  18580  mreclatdemoBAD  18675  mnfnei  18800  resthauslem  18942  sshauslem  18951  discmp  18976  conima  19004  1stcfb  19024  hauseqlcld  19194  xkoptsub  19202  xkofvcn  19232  idqtop  19254  tgqtop  19260  kqdisj  19280  xpstopnlem1  19357  xpstopnlem2  19359  ufildom1  19474  alexsubb  19593  alexsubALTlem3  19596  ptcmplem2  19600  ptcmplem3  19601  tmdgsum  19641  ustneism  19773  ustuqtop1  19791  iducn  19833  prdsmet  19920  imasdsf1olem  19923  xpsxmet  19930  xpsdsval  19931  xpsmet  19932  prdsbl  20041  met1stc  20071  prdsxmslem2  20079  xpsxms  20084  xpsms  20085  dscmet  20140  nmoffn  20265  nmofval  20268  nmolb  20271  nmof  20273  cnbl0  20328  xrsmopn  20364  xrge0gsumle  20385  xrge0tsms  20386  negfcncf  20470  cnrehmeo  20500  lebnum  20511  xlebnum  20512  reparphti  20544  pcopt  20569  pcopt2  20570  pcorevcl  20572  pcorevlem  20573  pi1xfrval  20601  pi1xfrcnvlem  20603  pi1xfrcnv  20604  pi1cof  20606  pi1coval  20607  nmhmcn  20650  cphsubrglem  20671  csscld  20736  cmetcaulem  20774  cmpcmet  20803  ovolunlem1  20955  ovolicc2lem4  20978  ioovolcl  21025  ioorcl2  21027  uniioovol  21034  uniioombllem4  21041  uniioombllem5  21042  uniioombllem6  21043  dyadmbllem  21054  mbfsub  21115  itg1climres  21167  xrge0f  21184  itg2ge0  21188  itg2i1fseq2  21209  ibl0  21239  ellimc2  21327  limcflf  21331  dvreslem  21359  dvidlem  21365  dvid  21367  cpnres  21386  dvaddbr  21387  dvmulbr  21388  dvfre  21400  dvexp  21402  dvrec  21404  dvmptid  21406  dvmptc  21407  dvmptntr  21420  dvexp3  21425  dvlipcn  21441  dveq0  21447  dv11cn  21448  lhop2  21462  ftc1a  21484  tdeglem1  21502  tdeglem3  21503  tdeglem4  21504  tdeglem2  21505  mdeg0  21516  mdegle0  21523  ply1remlem  21609  fta1glem2  21613  plypf1  21655  coe0  21698  dvply1  21725  elqaalem3  21762  aaliou2b  21782  aaliou3lem8  21786  aaliou3lem7  21790  taylfvallem  21798  taylf  21801  tayl0  21802  taylpfval  21805  taylply  21809  dvtaylp  21810  taylthlem1  21813  taylthlem2  21814  ulmdvlem1  21840  ulmdvlem2  21841  ulmdvlem3  21842  radcnvcl  21857  psercnlem2  21864  psercn  21866  pserdv  21869  abelthlem3  21873  abelth  21881  sincn  21884  coscn  21885  reefgim  21890  tangtx  21942  pige3  21954  cosordlem  21962  logcn  22067  dvlog  22071  advlog  22074  advlogexp  22075  logtayl  22080  logccv  22083  dvcxp1  22155  cxpcn3lem  22160  cxpcn3  22161  resqrcn  22162  sqrcn  22163  loglesqr  22171  isosctrlem2  22192  dquartlem1  22221  quart  22231  atancj  22280  efiatan  22282  atantan  22293  atanbndlem  22295  atansopn  22302  dvatan  22305  atantayl  22307  leibpilem2  22311  leibpi  22312  log2tlbnd  22315  rlimcnp2  22335  efrlim  22338  divsqrsumlem  22348  jensenlem1  22355  jensenlem2  22356  jensen  22357  amgmlem  22358  amgm  22359  emcllem4  22367  emcllem7  22370  wilthlem2  22382  wilthlem3  22383  basellem6  22398  chtrpcl  22488  ppiltx  22490  1sgm2ppw  22514  chtlepsi  22520  chpub  22534  logfacbnd3  22537  logfacrlim  22538  perfectlem2  22544  dchrelbas2  22551  dchrabs  22574  dchrhash  22585  bposlem7  22604  lgsdir2lem5  22641  lgsqrlem1  22655  lgseisenlem4  22666  lgsquad2lem1  22672  lgsquad3  22675  chpo1ub  22704  vmadivsumb  22707  rpvmasumlem  22711  dchrisumlem2  22714  dchrmusumlema  22717  dchrvmasumlem2  22722  dchrvmasumlema  22724  dchrvmasumiflem1  22725  dchrisum0flblem1  22732  dchrisum0lem1  22740  rplogsum  22751  mudivsum  22754  logdivsum  22757  mulog2sumlem2  22759  vmalogdivsum2  22762  2vmadivsumlem  22764  log2sumbnd  22768  selberglem2  22770  selbergb  22773  selberg2lem  22774  selberg2b  22776  selberg3lem1  22781  selberg4lem1  22784  selberg4  22785  pntrsumo1  22789  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntibndlem1  22813  pntibndlem2  22815  pntibndlem3  22816  pntlemb  22821  pntlemr  22826  pntlemf  22829  pntlem3  22833  pnt  22838  qabvle  22849  padicabv  22854  ostth1  22857  uhgrares  23193  umgrares  23209  usgrares  23239  nbgraop  23286  nbgraf1o0  23306  cusgra0v  23319  cusgra1v  23320  cusgraexilem2  23326  sizeusglecusg  23345  isuvtx  23347  2trllemH  23402  wlkntrllem3  23411  2wlklem1  23447  constr3trllem3  23489  constr3pthlem3  23494  vdgr0  23521  eupatrl  23540  eupares  23547  vdegp1ai  23556  vdegp1bi  23557  vsfval  23964  ipasslem7  24187  minvecolem2  24227  h2hcau  24332  h2hlm  24333  hlimadd  24546  hhsscms  24631  chocunii  24655  occllem  24657  leopnmid  25493  opsqrlem1  25495  hmopidmchi  25506  mdslj1i  25674  addltmulALT  25801  imadifxp  25890  xaddeq0  25997  xrge0npcan  26108  xrge0tsmsd  26204  xpinpreima2  26289  cnre2csqlem  26292  tpr2rico  26294  ordtrestNEW  26303  mndpluscn  26308  pnfneige0  26333  qqhghm  26369  qqhrhm  26370  qqhcn  26372  qqhucn  26373  rrhre  26399  esumsplit  26458  esumpr  26468  esumfsup  26471  sigaclcu2  26515  pwsiga  26525  prsiga  26526  measvuni  26580  elmbfmvol2  26634  mbfmcnt  26635  sxbrsigalem1  26652  sxbrsiga  26657  omsfval  26661  sibf0  26672  sitgclg  26680  eulerpartgbij  26707  eulerpartlemgh  26713  isrrvv  26778  rrvadd  26787  rrvmulc  26788  dstrvprob  26806  coinflipspace  26815  coinfliprv  26817  ballotlemfmpn  26829  ballotlem1ri  26869  signsplypnf  26903  signsply0  26904  signswrid  26911  lgamcvg2  26993  gamcvg2lem  26997  indispcon  27075  conpcon  27076  iccllyscon  27091  cvmopnlem  27119  cvmliftlem15  27139  cvmlift2lem3  27146  circum  27270  fprodfac  27434  fallfac0  27482  bpoly4  28153  elhf2  28164  finixpnum  28367  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  dvtan  28395  itg2addnclem  28396  ftc1anclem5  28424  dvcncxp1  28430  dvasin  28433  dvreasin  28435  dvreacos  28436  areacirclem1  28437  areacirc  28442  bnd2lem  28643  prdsbnd  28645  cntotbnd  28648  cnpwstotbnd  28649  isdrngo2  28717  prter2  28979  isnacs3  28999  diophrw  29050  lzenom  29061  diophin  29064  pellexlem5  29127  pw2f1ocnv  29339  dnnumch2  29351  kelac2lem  29370  kelac2  29371  dfac21  29372  pwfi2f1o  29404  frlmpwfi  29406  mpaaeu  29460  rngunsnply  29483  mendbas  29494  mendplusgfval  29495  mendmulrfval  29497  mendsca  29499  mendvscafval  29500  subrgacs  29510  sdrgacs  29511  cntzsdrg  29512  idomodle  29514  phisum  29520  proot1ex  29522  deg1mhm  29528  itgpowd  29543  ofsubid  29551  ofdivrec  29553  dvconstbi  29561  stoweidlem13  29761  stoweidlem26  29774  stoweidlem34  29782  stoweidlem42  29790  stoweidlem44  29792  stoweidlem48  29796  stoweidlem62  29810  stoweid  29811  stirlinglem7  29828  stirlinglem11  29832  fvelrnfvelrnressn  30104  modfsummods  30197  lswccats1fst  30215  usg2wlkeq  30242  usgra2wlkspthlem1  30249  usgra2wlkspthlem2  30250  wwlkn  30269  wlkiswwlk2  30284  wwlkn0s  30292  wwlkexthasheq  30319  wlknwwlknvbij  30325  clwwlkn  30383  clwwlkn2  30391  clwlkisclwwlklem2  30401  clwwlkvbij  30416  scshwfzeqfzo  30445  eclclwwlkn0  30458  hashecclwwlkn1  30461  usghashecclwwlk  30462  rusgrasn  30510  frgra3v  30547  frgrancvvdeqlem9  30587  frgrancvvdgeq  30589  frg2wot1  30603  usgreghash2spotv  30612  extwwlkfablem2  30624  numclwwlkovf2  30630  numclwwlk2lem3  30652  altgsumbcALT  30701  zlmodzxzel  30703  zlmodzxzsubm  30707  zlmodzxzsub  30708  gsumpr  30709  psgnsn  30722  isnzr2hash  30725  scmsuppss  30736  coe1fsupp  30769  mat1dimelbas  30790  m1detdiag  30823  lcoop  30834  lincval0  30838  lco0  30850  linds0  30888  snlindsntorlem  30893  rng1nnzr  30915  lmod1lem2  30919  lmod1lem3  30920  lmod1zr  30924  lmod1zrnlvec  30925  zlmodzxznm  30928  zlmodzxzldeplem4  30934  eqlkr2  32585  tendoidcl  34253  cdlemk56  34455  dihpN  34821  mapdhval  35209  hlhillcs  35446
  Copyright terms: Public domain W3C validator