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  5320  relcoi2  5463  isomin  6127  isoini  6128  supp0  6795  suppval1  6796  suppssr  6820  dmtpos  6857  mpt2curryd  6888  oaabs2  7184  mapsncnv  7359  boxcutc  7406  domunsncan  7511  pw2f1o  7516  unxpdom2  7622  sucxpdom  7623  findcard2d  7655  ac6sfi  7657  xpfi  7684  imafi  7705  snopfsupp  7744  fifo  7783  ordtypelem4  7836  oismo  7855  wofib  7860  brwdom2  7889  canthwdom  7895  cantnffvalOLD  7972  cantnfval  7977  cantnflt  7981  cantnff  7983  cantnf0  7984  cantnfp1lem1  7987  cantnfp1lem3  7989  cantnflem1b  7995  cantnflem1  7998  cantnfltOLD  8011  cantnfp1lem1OLD  8013  cantnfp1lem3OLD  8015  cantnflem1bOLD  8018  cantnflem1dOLD  8020  cantnflem1OLD  8021  cnfcom  8034  cnfcom2lem  8035  cnfcomOLD  8042  cnfcom2lemOLD  8043  ranksnb  8135  tskwe  8221  cardidm  8230  infxpenc  8285  infxpencOLD  8290  fseqdom  8297  dfac8clem  8303  dfac12lem2  8414  infmap2  8488  isfin4-3  8585  fin23lem14  8603  fin23lem40  8621  isf34lem7  8649  isf34lem6  8650  fin1a2lem12  8681  hsmexlem4  8699  hsmexlem5  8700  ac5b  8748  alephexp1  8844  alephsuc3  8845  axpowndlem2OLD  8864  fpwwe2lem8  8905  fpwwe2lem13  8910  canthwe  8919  canthp1lem2  8921  gchcda1  8924  pwfseqlem5  8931  wunco  9001  prlem934  9303  supsrlem  9379  msqge0  9962  ofnegsub  10421  ofsubge0  10422  xaddpnf1  11297  supxrmnf  11381  injresinjlem  11739  uzindi  11904  seqfeq4  11956  seqof  11964  bcval5  12195  hashdomi  12245  hash1snb  12273  brfi1uzind  12321  lsw0  12369  ccatlen  12377  lswccatn0lsw  12389  s111  12404  swrdspsleq  12444  wrdeqswrdlsw  12445  wrdeqs1cat  12471  reps  12510  repsw0  12517  repswccat  12525  repswrevw  12526  lswcshw  12551  cshwsexa  12560  wrdlen2i  12648  shftfib  12663  limsupcl  13053  limsupgf  13055  limsupval2  13060  isercolllem3  13246  ackbijnn  13393  supcvg  13420  ege2le3  13477  rpnnen2lem5  13603  ruclem11  13624  fsumdvds  13678  bitsinv2  13741  sadaddlem  13764  smupf  13776  smup0  13777  smu01lem  13783  isprm6  13897  hashdvds  13952  reumodprminv  13974  vdwlem13  14156  ramtlecl  14163  0ram  14183  cshwshashnsame  14232  prmlem0  14235  wunndx  14292  prdsval  14495  xpsbas  14614  xpsadd  14616  xpsmul  14617  xpssca  14618  xpsvsca  14619  xpsless  14620  xpsle  14621  mreexexlem2d  14685  mreacs  14698  acsfn  14699  idfu2nd  14889  idfucl  14893  fucsect  14984  setccatid  15054  setcepi  15058  catchomfval  15068  uncfval  15146  oduglb  15411  odumeet  15412  odulub  15413  odujoin  15414  isipodrs  15433  fpwipodrs  15436  isacs4lem  15440  isacs5lem  15441  submacs  15595  frmdup1  15644  mulgneg2  15756  subgacs  15818  nsgacs  15819  idrespermg  16018  psgnunilem5  16102  psgnsn  16128  odf1o2  16176  frgpuplem  16373  cygctb  16472  gsumzunsnd  16556  gsum2dlem2  16567  gsum2dOLD  16569  dprdsubg  16626  dmdprdsplit2lem  16649  dmdprdpr  16653  dprdpr  16654  dpjeq  16663  dpjeqOLD  16670  ablfac1eulem  16678  pgpfac1lem2  16681  pgpfaclem1  16687  srgbinomlem4  16747  unitgrp  16865  isirred  16897  mptscmfsupp0  17117  lssacs  17154  pwssplit1  17246  lbsextlem2  17346  lbsextlem3  17347  psrass1lem  17553  psrlidm  17580  psrlidmOLD  17581  resspsradd  17595  resspsrmul  17596  resspsrvsca  17597  mplcoe5lem  17654  ltbwe  17661  psropprmul  17800  coe1add  17825  coe1mul2lem1  17828  coe1tm  17834  evls1rhmlem  17865  evl1sca  17877  evl1var  17879  pf1mpf  17895  pf1ind  17898  xrsmcmn  17948  xrs1mnd  17960  xrs10  17961  gsumfsum  17988  zringlpir  18015  zringcyg  18016  zlpirlem3  18019  zlpir  18020  zcyg  18021  mulgrhmOLD  18038  mulgrhm2OLD  18039  zndvds  18091  regsumsupp  18161  uvcvv1  18323  lsslinds  18369  matmulr  18422  mat0dimbas0  18434  ofco2  18443  mavmul0  18474  mavmul0g  18475  m1detdiag  18519  mdetunilem9  18542  maducoeval2  18562  madugsum  18565  smadiadetlem0  18583  smadiadetlem1a  18585  smadiadetlem4  18591  smadiadetglem1  18593  smadiadetglem2  18594  smadiadetg  18595  cramer0  18612  indistopon  18721  mreclatdemoBAD  18816  mnfnei  18941  resthauslem  19083  sshauslem  19092  discmp  19117  conima  19145  1stcfb  19165  hauseqlcld  19335  xkoptsub  19343  xkofvcn  19373  idqtop  19395  tgqtop  19401  kqdisj  19421  xpstopnlem1  19498  xpstopnlem2  19500  ufildom1  19615  alexsubb  19734  alexsubALTlem3  19737  ptcmplem2  19741  ptcmplem3  19742  tmdgsum  19782  ustneism  19914  ustuqtop1  19932  iducn  19974  prdsmet  20061  imasdsf1olem  20064  xpsxmet  20071  xpsdsval  20072  xpsmet  20073  prdsbl  20182  met1stc  20212  prdsxmslem2  20220  xpsxms  20225  xpsms  20226  dscmet  20281  nmoffn  20406  nmofval  20409  nmolb  20412  nmof  20414  cnbl0  20469  xrsmopn  20505  xrge0gsumle  20526  xrge0tsms  20527  negfcncf  20611  cnrehmeo  20641  lebnum  20652  xlebnum  20653  reparphti  20685  pcopt  20710  pcopt2  20711  pcorevcl  20713  pcorevlem  20714  pi1xfrval  20742  pi1xfrcnvlem  20744  pi1xfrcnv  20745  pi1cof  20747  pi1coval  20748  nmhmcn  20791  cphsubrglem  20812  csscld  20877  cmetcaulem  20915  cmpcmet  20944  ovolunlem1  21096  ovolicc2lem4  21119  ioovolcl  21166  ioorcl2  21168  uniioovol  21175  uniioombllem4  21182  uniioombllem5  21183  uniioombllem6  21184  dyadmbllem  21195  mbfsub  21256  itg1climres  21308  xrge0f  21325  itg2ge0  21329  itg2i1fseq2  21350  ibl0  21380  ellimc2  21468  limcflf  21472  dvreslem  21500  dvidlem  21506  dvid  21508  cpnres  21527  dvaddbr  21528  dvmulbr  21529  dvfre  21541  dvexp  21543  dvrec  21545  dvmptid  21547  dvmptc  21548  dvmptntr  21561  dvexp3  21566  dvlipcn  21582  dveq0  21588  dv11cn  21589  lhop2  21603  ftc1a  21625  tdeglem1  21643  tdeglem3  21644  tdeglem4  21645  tdeglem2  21646  mdeg0  21657  mdegle0  21664  ply1remlem  21750  fta1glem2  21754  plypf1  21796  coe0  21839  dvply1  21866  elqaalem3  21903  aaliou2b  21923  aaliou3lem8  21927  aaliou3lem7  21931  taylfvallem  21939  taylf  21942  tayl0  21943  taylpfval  21946  taylply  21950  dvtaylp  21951  taylthlem1  21954  taylthlem2  21955  ulmdvlem1  21981  ulmdvlem2  21982  ulmdvlem3  21983  radcnvcl  21998  psercnlem2  22005  psercn  22007  pserdv  22010  abelthlem3  22014  abelth  22022  sincn  22025  coscn  22026  reefgim  22031  tangtx  22083  pige3  22095  cosordlem  22103  logcn  22208  dvlog  22212  advlog  22215  advlogexp  22216  logtayl  22221  logccv  22224  dvcxp1  22296  cxpcn3lem  22301  cxpcn3  22302  resqrcn  22303  sqrcn  22304  loglesqr  22312  isosctrlem2  22333  dquartlem1  22362  quart  22372  atancj  22421  efiatan  22423  atantan  22434  atanbndlem  22436  atansopn  22443  dvatan  22446  atantayl  22448  leibpilem2  22452  leibpi  22453  log2tlbnd  22456  rlimcnp2  22476  efrlim  22479  divsqrsumlem  22489  jensenlem1  22496  jensenlem2  22497  jensen  22498  amgmlem  22499  amgm  22500  emcllem4  22508  emcllem7  22511  wilthlem2  22523  wilthlem3  22524  basellem6  22539  chtrpcl  22629  ppiltx  22631  1sgm2ppw  22655  chtlepsi  22661  chpub  22675  logfacbnd3  22678  logfacrlim  22679  perfectlem2  22685  dchrelbas2  22692  dchrabs  22715  dchrhash  22726  bposlem7  22745  lgsdir2lem5  22782  lgsqrlem1  22796  lgseisenlem4  22807  lgsquad2lem1  22813  lgsquad3  22816  chpo1ub  22845  vmadivsumb  22848  rpvmasumlem  22852  dchrisumlem2  22855  dchrmusumlema  22858  dchrvmasumlem2  22863  dchrvmasumlema  22865  dchrvmasumiflem1  22866  dchrisum0flblem1  22873  dchrisum0lem1  22881  rplogsum  22892  mudivsum  22895  logdivsum  22898  mulog2sumlem2  22900  vmalogdivsum2  22903  2vmadivsumlem  22905  log2sumbnd  22909  selberglem2  22911  selbergb  22914  selberg2lem  22915  selberg2b  22917  selberg3lem1  22922  selberg4lem1  22925  selberg4  22926  pntrsumo1  22930  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntibndlem1  22954  pntibndlem2  22956  pntibndlem3  22957  pntlemb  22962  pntlemr  22967  pntlemf  22970  pntlem3  22974  pnt  22979  qabvle  22990  padicabv  22995  ostth1  22998  istrkg2ld  23038  perpln1  23229  perpln2  23230  isperp  23231  uhgrares  23377  umgrares  23393  usgrares  23423  nbgraop  23470  nbgraf1o0  23490  cusgra0v  23503  cusgra1v  23504  cusgraexilem2  23510  sizeusglecusg  23529  isuvtx  23531  2trllemH  23586  wlkntrllem3  23595  2wlklem1  23631  constr3trllem3  23673  constr3pthlem3  23678  vdgr0  23705  eupatrl  23724  eupares  23731  vdegp1ai  23740  vdegp1bi  23741  vsfval  24148  ipasslem7  24371  minvecolem2  24411  h2hcau  24516  h2hlm  24517  hlimadd  24730  hhsscms  24815  chocunii  24839  occllem  24841  leopnmid  25677  opsqrlem1  25679  hmopidmchi  25690  mdslj1i  25858  addltmulALT  25985  imadifxp  26073  xaddeq0  26180  xrge0npcan  26291  xrge0tsmsd  26387  xpinpreima2  26471  cnre2csqlem  26474  tpr2rico  26476  ordtrestNEW  26485  mndpluscn  26490  pnfneige0  26515  qqhghm  26551  qqhrhm  26552  qqhcn  26554  qqhucn  26555  rrhre  26581  esumsplit  26640  esumpr  26650  esumfsup  26653  sigaclcu2  26697  pwsiga  26707  prsiga  26708  measvuni  26762  elmbfmvol2  26816  mbfmcnt  26817  sxbrsigalem1  26834  sxbrsiga  26839  omsfval  26843  sibf0  26854  sitgclg  26862  eulerpartgbij  26889  eulerpartlemgh  26895  isrrvv  26960  rrvadd  26969  rrvmulc  26970  dstrvprob  26988  coinflipspace  26997  coinfliprv  26999  ballotlemfmpn  27011  ballotlem1ri  27051  signsplypnf  27085  signsply0  27086  signswrid  27093  lgamcvg2  27175  gamcvg2lem  27179  indispcon  27257  conpcon  27258  iccllyscon  27273  cvmopnlem  27301  cvmliftlem15  27321  cvmlift2lem3  27328  circum  27453  fprodfac  27617  fallfac0  27665  bpoly4  28336  elhf2  28347  finixpnum  28552  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  ovoliunnfl  28571  voliunnfl  28573  volsupnfl  28574  dvtan  28580  itg2addnclem  28581  ftc1anclem5  28609  dvcncxp1  28615  dvasin  28618  dvreasin  28620  dvreacos  28621  areacirclem1  28622  areacirc  28627  bnd2lem  28828  prdsbnd  28830  cntotbnd  28833  cnpwstotbnd  28834  isdrngo2  28902  prter2  29164  isnacs3  29184  diophrw  29235  lzenom  29246  diophin  29249  pellexlem5  29312  pw2f1ocnv  29524  dnnumch2  29536  kelac2lem  29555  kelac2  29556  dfac21  29557  pwfi2f1o  29589  frlmpwfi  29591  mpaaeu  29645  rngunsnply  29668  mendbas  29679  mendplusgfval  29680  mendmulrfval  29682  mendsca  29684  mendvscafval  29685  subrgacs  29695  sdrgacs  29696  cntzsdrg  29697  idomodle  29699  phisum  29705  proot1ex  29707  deg1mhm  29713  itgpowd  29728  ofsubid  29736  ofdivrec  29738  dvconstbi  29746  stoweidlem13  29946  stoweidlem26  29959  stoweidlem34  29967  stoweidlem42  29975  stoweidlem44  29977  stoweidlem48  29981  stoweidlem62  29995  stoweid  29996  stirlinglem7  30013  stirlinglem11  30017  fvelrnfvelrnressn  30289  modfsummods  30382  lswccats1fst  30400  usg2wlkeq  30427  usgra2wlkspthlem1  30434  usgra2wlkspthlem2  30435  wwlkn  30454  wlkiswwlk2  30469  wwlkn0s  30477  wwlkexthasheq  30504  wlknwwlknvbij  30510  clwwlkn  30568  clwwlkn2  30576  clwlkisclwwlklem2  30586  clwwlkvbij  30601  scshwfzeqfzo  30630  eclclwwlkn0  30643  hashecclwwlkn1  30646  usghashecclwwlk  30647  rusgrasn  30695  frgra3v  30732  frgrancvvdeqlem9  30772  frgrancvvdgeq  30774  frg2wot1  30788  usgreghash2spotv  30797  extwwlkfablem2  30809  numclwwlkovf2  30815  numclwwlk2lem3  30837  altgsumbcALT  30888  zlmodzxzel  30890  zlmodzxzsubm  30894  zlmodzxzsub  30895  gsumpr  30896  isnzr2hash  30912  scmsuppss  30923  gsummptnn0fz  30947  coe1fsupp  30973  ply1mulgsum  30990  mat1dimelbas  31021  lcoop  31052  lincval0  31056  lco0  31068  linds0  31106  snlindsntorlem  31111  rng1nnzr  31133  lmod1lem2  31137  lmod1lem3  31138  lmod1zr  31142  lmod1zrnlvec  31143  zlmodzxznm  31146  zlmodzxzldeplem4  31152  cpmat  31172  mat2pmatfval  31186  m2pminv2lem  31212  pmatcollpw4  31240  pmatcollpw4fi  31241  pmatcollpw4fi1lem2  31243  pmatcollpw4fi1  31244  pmattomply1rn  31257  idpmattoidmply1  31260  pmattomply1mhmlem2  31274  cpmatfval  31283  chfacfscmulfsupp  31313  chfacfpmmulfsupp  31317  cpmidpmatlem2  31325  cpmadugsumlemF  31330  cpmadumatpolylem1  31335  cayhamlem3  31342  cayhamlem4  31343  eqlkr2  33051  tendoidcl  34719  cdlemk56  34921  dihpN  35287  mapdhval  35675  hlhillcs  35912
  Copyright terms: Public domain W3C validator