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  5381  relcoi2  5525  fvrnressn  6071  isomin  6218  isoini  6219  supp0  6908  suppval1  6909  suppssr  6933  dmtpos  6969  mpt2curryd  7000  oaabs2  7296  mapsncnv  7467  boxcutc  7514  domunsncan  7619  pw2f1o  7624  unxpdom2  7730  sucxpdom  7731  findcard2d  7764  ac6sfi  7766  xpfi  7793  imafi  7815  snopfsupp  7854  fifo  7894  ordtypelem4  7949  oismo  7968  wofib  7973  brwdom2  8002  canthwdom  8008  cantnffvalOLD  8085  cantnfval  8090  cantnflt  8094  cantnff  8096  cantnf0  8097  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1  8111  cantnfltOLD  8124  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1dOLD  8133  cantnflem1OLD  8134  cnfcom  8147  cnfcom2lem  8148  cnfcomOLD  8155  cnfcom2lemOLD  8156  ranksnb  8248  tskwe  8334  cardidm  8343  infxpenc  8398  infxpencOLD  8403  fseqdom  8410  dfac8clem  8416  dfac12lem2  8527  infmap2  8601  isfin4-3  8698  fin23lem14  8716  fin23lem40  8734  isf34lem7  8762  isf34lem6  8763  fin1a2lem12  8794  hsmexlem4  8812  hsmexlem5  8813  ac5b  8861  alephexp1  8957  alephsuc3  8958  axpowndlem2OLD  8977  fpwwe2lem8  9018  fpwwe2lem13  9023  canthwe  9032  canthp1lem2  9034  gchcda1  9037  pwfseqlem5  9044  wunco  9114  prlem934  9414  supsrlem  9491  msqge0  10081  ofnegsub  10541  ofsubge0  10542  xaddpnf1  11436  supxrmnf  11520  injresinjlem  11907  uzindi  12073  seqfeq4  12138  seqof  12146  bcval5  12378  hashdomi  12430  hash1snb  12461  brfi1uzind  12514  lsw0  12568  ccatlen  12576  lswccatn0lsw  12589  s111  12605  lswccats1fst  12621  swrdspsleq  12655  wrdeqswrdlsw  12656  wrdeqs1cat  12682  reps  12724  repsw0  12731  repswccat  12739  repswrevw  12740  lswcshw  12765  cshwsexa  12774  scshwfzeqfzo  12776  wrdlen2i  12866  shftfib  12887  limsupcl  13278  limsupgf  13280  limsupval2  13285  isercolllem3  13471  modfsummods  13589  ackbijnn  13622  supcvg  13649  fprodfac  13759  ege2le3  13807  rpnnen2lem5  13934  ruclem11  13955  fsumdvds  14011  bitsinv2  14075  sadaddlem  14098  smupf  14110  smup0  14111  smu01lem  14117  isprm6  14232  hashdvds  14287  reumodprminv  14311  prmreclem6  14421  vdwlem13  14493  ramtlecl  14500  0ram  14520  cshwshashnsame  14570  prmlem0  14573  wunndx  14630  prdsval  14834  xpsbas  14953  xpsadd  14955  xpsmul  14956  xpssca  14957  xpsvsca  14958  xpsless  14959  xpsle  14960  mreexexlem2d  15024  mreacs  15037  acsfn  15038  idfu2nd  15225  idfucl  15229  fucsect  15320  setccatid  15390  setcepi  15394  catchomfval  15404  uncfval  15482  oduglb  15748  odumeet  15749  odulub  15750  odujoin  15751  isipodrs  15770  fpwipodrs  15773  isacs4lem  15777  isacs5lem  15778  idmhm  15954  submacs  15975  frmdup1  16011  mgmnsgrpex  16028  mulgneg2  16148  subgacs  16215  nsgacs  16216  idrespermg  16415  psgnunilem5  16498  psgnsn  16524  odf1o2  16572  frgpuplem  16769  cygctb  16873  gsumzunsnd  16961  gsum2dlem2  16977  gsum2dOLD  16979  gsummptnn0fz  16993  dprdsubg  17050  dmdprdsplit2lem  17073  dmdprdpr  17077  dprdpr  17078  dpjeq  17087  dpjeqOLD  17094  ablfac1eulem  17102  pgpfac1lem2  17105  pgpfaclem1  17111  srgbinomlem4  17173  unitgrp  17295  isirred  17327  brric  17372  mptscmfsupp0  17555  lssacs  17592  pwssplit1  17684  lbsextlem2  17784  lbsextlem3  17785  isnzr2hash  17891  0ring01eqbi  17900  rng1nnzr  17901  psrass1lem  18008  psrlidm  18035  psrlidmOLD  18036  resspsradd  18050  resspsrmul  18051  resspsrvsca  18052  mplcoe5lem  18109  ltbwe  18116  coe1fsupp  18233  psropprmul  18258  coe1add  18284  coe1mul2lem1  18287  coe1tm  18293  cply1coe0bi  18321  evls1rhmlem  18337  evl1sca  18349  evl1var  18351  pf1mpf  18367  pf1ind  18370  xrsmcmn  18420  xrs1mnd  18435  xrs10  18436  gsumfsum  18463  zringlpir  18490  zringcyg  18491  zlpirlem3  18494  zlpir  18495  zcyg  18496  mulgrhmOLD  18513  mulgrhm2OLD  18514  zndvds  18566  regsumsupp  18636  uvcvv1  18798  lsslinds  18844  matmulr  18918  ofco2  18931  mat0dimbas0  18946  mat1dimelbas  18951  mat1f1o  18958  dmatval  18972  scmatghm  19013  mavmul0  19032  mavmul0g  19033  m1detdiag  19077  mdetunilem9  19100  maducoeval2  19120  madugsum  19123  smadiadetlem0  19141  smadiadetlem1a  19143  smadiadetlem4  19149  smadiadetglem1  19151  smadiadetglem2  19152  smadiadetg  19153  cramer0  19170  cpmat  19188  mat2pmatfval  19202  cpm2mfval  19228  m2cpminvid2lem  19233  pmatcollpw3fi1lem2  19266  pmatcollpw3fi1  19267  idpm2idmp  19280  pm2mpmhmlem2  19298  chpmatfval  19309  chfacfscmulfsupp  19338  chfacfpmmulfsupp  19342  cpmidpmatlem2  19350  cpmadugsumlemF  19355  cpmidgsum2  19358  cpmadumatpolylem1  19360  cayhamlem3  19366  cayhamlem4  19367  indistopon  19480  mreclatdemoBAD  19575  mnfnei  19700  resthauslem  19842  sshauslem  19851  discmp  19876  conima  19904  1stcfb  19924  hauseqlcld  20125  xkoptsub  20133  xkofvcn  20163  idqtop  20185  tgqtop  20191  kqdisj  20211  xpstopnlem1  20288  xpstopnlem2  20290  ufildom1  20405  alexsubb  20524  alexsubALTlem3  20527  ptcmplem2  20531  ptcmplem3  20532  tmdgsum  20572  ustneism  20704  ustuqtop1  20722  iducn  20764  prdsmet  20851  imasdsf1olem  20854  xpsxmet  20861  xpsdsval  20862  xpsmet  20863  prdsbl  20972  met1stc  21002  prdsxmslem2  21010  xpsxms  21015  xpsms  21016  psmetutop  21064  dscmet  21071  nmoffn  21196  nmofval  21199  nmolb  21202  nmof  21204  cnbl0  21259  xrsmopn  21295  xrge0gsumle  21316  xrge0tsms  21317  negfcncf  21401  cnrehmeo  21431  lebnum  21442  xlebnum  21443  reparphti  21475  pcopt  21500  pcopt2  21501  pcorevcl  21503  pcorevlem  21504  pi1xfrval  21532  pi1xfrcnvlem  21534  pi1xfrcnv  21535  pi1cof  21537  pi1coval  21538  nmhmcn  21581  cphsubrglem  21602  csscld  21667  cmetcaulem  21705  cmpcmet  21734  ovolunlem1  21886  ovolicc2lem4  21909  ioovolcl  21957  ioorcl2  21959  uniioovol  21966  uniioombllem4  21973  uniioombllem5  21974  uniioombllem6  21975  dyadmbllem  21986  mbfsub  22047  itg1climres  22099  xrge0f  22116  itg2ge0  22120  itg2i1fseq2  22141  ibl0  22171  ellimc2  22259  limcflf  22263  dvreslem  22291  dvidlem  22297  dvid  22299  cpnres  22318  dvaddbr  22319  dvmulbr  22320  dvfre  22332  dvexp  22334  dvrec  22336  dvmptid  22338  dvmptc  22339  dvmptntr  22352  dvexp3  22357  dvlipcn  22373  dveq0  22379  dv11cn  22380  lhop2  22394  ftc1a  22416  tdeglem1  22434  tdeglem3  22435  tdeglem4  22436  tdeglem2  22437  mdeg0  22448  mdegle0  22455  ply1remlem  22541  fta1glem2  22545  plypf1  22587  coe0  22631  dvply1  22658  elqaalem3  22695  aaliou2b  22715  aaliou3lem8  22719  aaliou3lem7  22723  taylfvallem  22731  taylf  22734  tayl0  22735  taylpfval  22738  taylply  22742  dvtaylp  22743  taylthlem1  22746  taylthlem2  22747  ulmdvlem1  22773  ulmdvlem2  22774  ulmdvlem3  22775  radcnvcl  22790  psercnlem2  22797  psercn  22799  pserdv  22802  abelthlem3  22806  abelth  22814  sincn  22817  coscn  22818  reefgim  22823  tangtx  22876  pige3  22888  cosordlem  22896  logcn  23006  dvlog  23010  advlog  23013  advlogexp  23014  logtayl  23019  logccv  23022  dvcxp1  23094  cxpcn3lem  23099  cxpcn3  23100  resqrtcn  23101  sqrtcn  23102  loglesqrt  23110  isosctrlem2  23131  dquartlem1  23160  quart  23170  atancj  23219  efiatan  23221  atantan  23232  atanbndlem  23234  atansopn  23241  dvatan  23244  atantayl  23246  leibpilem2  23250  leibpi  23251  log2tlbnd  23254  rlimcnp2  23274  efrlim  23277  divsqrtsumlem  23287  jensenlem1  23294  jensenlem2  23295  jensen  23296  amgmlem  23297  amgm  23298  emcllem4  23306  emcllem7  23309  wilthlem2  23321  wilthlem3  23322  basellem6  23337  chtrpcl  23427  ppiltx  23429  1sgm2ppw  23453  chtlepsi  23459  chpub  23473  logfacbnd3  23476  logfacrlim  23477  perfectlem2  23483  dchrelbas2  23490  dchrabs  23513  dchrhash  23524  bposlem7  23543  lgsdir2lem5  23580  lgsqrlem1  23594  lgseisenlem4  23605  lgsquad2lem1  23611  lgsquad3  23614  chpo1ub  23643  vmadivsumb  23646  rpvmasumlem  23650  dchrisumlem2  23653  dchrmusumlema  23656  dchrvmasumlem2  23661  dchrvmasumlema  23663  dchrvmasumiflem1  23664  dchrisum0flblem1  23671  dchrisum0lem1  23679  rplogsum  23690  mudivsum  23693  logdivsum  23696  mulog2sumlem2  23698  vmalogdivsum2  23701  2vmadivsumlem  23703  log2sumbnd  23707  selberglem2  23709  selbergb  23712  selberg2lem  23713  selberg2b  23715  selberg3lem1  23720  selberg4lem1  23723  selberg4  23724  pntrsumo1  23728  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  pntibndlem1  23752  pntibndlem2  23754  pntibndlem3  23755  pntlemb  23760  pntlemr  23765  pntlemf  23768  pntlem3  23772  pnt  23777  qabvle  23788  padicabv  23793  ostth1  23796  istrkg2ld  23836  tgldimor  23871  motgrp  23908  perpln1  24065  perpln2  24066  isperp  24067  uhgrares  24286  umgrares  24302  edgopval  24318  usgrares  24347  nbgraop  24401  nbgraopALT  24402  nbgraf1o0  24424  cusgra0v  24438  cusgra1v  24439  cusgraexilem2  24445  sizeusglecusg  24464  isuvtx  24466  2trllemH  24532  wlkntrllem3  24541  2wlklem1  24577  usgra2wlkspthlem1  24597  usgra2wlkspthlem2  24598  constr3trllem3  24630  constr3pthlem3  24635  wwlkn  24660  wlkiswwlk2  24675  wwlkn0s  24683  usg2wlkeq  24686  wwlkexthasheq  24712  wlknwwlknvbij  24718  clwwlkn  24745  clwwlkn2  24753  clwlkisclwwlklem2  24764  clwwlkvbij  24779  eclclwwlkn0  24809  hashecclwwlkn1  24812  usghashecclwwlk  24813  vdgr0  24878  rusgrasn  24923  eupatrl  24946  eupares  24953  vdegp1ai  24962  vdegp1bi  24963  frgra3v  24980  frgrancvvdeqlem9  25019  frgrancvvdgeq  25021  frg2wot1  25035  usgreghash2spotv  25044  extwwlkfablem2  25056  numclwwlkovf2  25062  numclwwlk2lem3  25084  vsfval  25506  ipasslem7  25729  minvecolem2  25769  h2hcau  25874  h2hlm  25875  hlimadd  26088  hhsscms  26173  chocunii  26197  occllem  26199  leopnmid  27035  opsqrlem1  27037  hmopidmchi  27048  mdslj1i  27216  addltmulALT  27343  imadifxp  27436  xaddeq0  27551  xrge0npcan  27662  gsumle  27748  gsummpt2co  27749  xrge0tsmsd  27753  locfinreflem  27821  locfinref  27822  xpinpreima2  27867  cnre2csqlem  27870  tpr2rico  27872  ordtrestNEW  27881  ordtrest2NEW  27883  mndpluscn  27886  pnfneige0  27911  qqhghm  27947  qqhrhm  27948  qqhcn  27950  qqhucn  27951  rrhcn  27956  rrhre  27977  esumsplit  28041  esumpr  28051  esumfsup  28054  sigaclcu2  28098  pwsiga  28108  prsiga  28109  measvuni  28163  elmbfmvol2  28216  mbfmcnt  28217  sxbrsigalem1  28234  sxbrsiga  28239  omsfval  28243  sibf0  28254  sitgclg  28262  sitmval  28268  eulerpartgbij  28289  eulerpartlemgh  28295  isrrvv  28360  rrvadd  28369  rrvmulc  28370  dstrvprob  28388  coinflipspace  28397  coinfliprv  28399  ballotlemfmpn  28411  ballotlem1ri  28451  sgnmulsgn  28466  plymul02  28481  signsplypnf  28485  signsply0  28486  signswrid  28493  lgamcvg2  28575  gamcvg2lem  28579  indispcon  28657  conpcon  28658  iccllyscon  28673  cvmopnlem  28701  cvmliftlem15  28721  cvmlift2lem3  28728  mrsubff  28850  mrsubccat  28856  circum  29018  fallfac0  29126  bpoly4  29797  elhf2  29808  finixpnum  30014  mblfinlem3  30029  mblfinlem4  30030  ismblfin  30031  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  dvtan  30041  itg2addnclem  30042  ftc1anclem5  30070  dvcncxp1  30076  dvasin  30079  dvreasin  30081  dvreacos  30082  areacirclem1  30083  areacirc  30088  bnd2lem  30263  prdsbnd  30265  cntotbnd  30268  cnpwstotbnd  30269  isdrngo2  30337  prter2  30598  isnacs3  30618  diophrw  30668  lzenom  30679  diophin  30682  pellexlem5  30745  pw2f1ocnv  30955  dnnumch2  30967  kelac2lem  30986  kelac2  30987  dfac21  30988  pwfi2f1o  31020  frlmpwfi  31022  mpaaeu  31075  rngunsnply  31098  mendbas  31109  mendplusgfval  31110  mendmulrfval  31112  mendsca  31114  mendvscafval  31115  subrgacs  31125  sdrgacs  31126  cntzsdrg  31127  idomodle  31129  phisum  31135  proot1ex  31137  deg1mhm  31143  itgpowd  31158  hashnzfzclim  31203  ofsubid  31205  ofdivrec  31207  dvconstbi  31215  fzisoeu  31454  sumnnodd  31590  negcncfg  31637  cnfdmsn  31638  divcncf  31640  dvmptresicc  31670  itgcoscmulx  31722  stoweidlem13  31749  stoweidlem26  31762  stoweidlem34  31770  stoweidlem42  31778  stoweidlem44  31780  stoweidlem48  31784  stoweidlem62  31798  stoweid  31799  stirlinglem7  31816  stirlinglem11  31820  stirlinglem12  31821  dirkeritg  31838  dirkercncflem2  31840  dirkercncflem4  31842  fourierdlem16  31859  fourierdlem21  31864  fourierdlem22  31865  fourierdlem24  31867  fourierdlem48  31891  fourierdlem49  31892  fourierdlem62  31905  fourierdlem70  31913  fourierdlem80  31923  fourierdlem83  31926  fourierdlem85  31928  fourierdlem102  31945  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  fourierdlem114  31957  uhgrepe  32332  uhgres  32333  gordopval  32344  gsizopval  32345  usgedgnlp  32364  isfusgracl  32380  isfusgraclALT  32382  usgo0s0  32389  usgo0s0ALT  32390  usgo1s0ALT  32391  usgo1s0  32396  usgresvm1  32397  usgfis  32400  usgresvm1ALT  32401  usgrafiedgALT  32405  idmgmhm  32430  mgmplusgiopALT  32471  sgrp2sgrp  32505  isrnghm  32533  lidlmmgm  32558  2zrngnmlid  32582  estrccatid  32604  estrreslem1  32609  estrreslem2  32610  estrres  32611  funcestrcsetclem8  32619  fullestrcsetc  32623  embedsetcestrclem  32629  funcsetcestrclem8  32634  dfrngc2  32655  rnghmsscmap2  32656  rnghmsscmap  32657  rngchomfvalOLD  32667  rngcidOLD  32674  funcrngcsetcALT  32682  dfringc2  32698  rhmsscmap2  32699  rhmsscmap  32700  rhmsscrnghm  32706  rngcresringcat  32710  funcringcsetcOLD2lem8  32723  ringchomfvalOLD  32727  ringcidOLD  32734  funcringcsetclem8OLD  32746  srhmsubc  32752  fldc  32759  rngcrescrhm  32761  rhmsubclem3  32764  srhmsubcOLD  32771  fldcOLD  32778  rngcrescrhmOLD  32780  altgsumbcALT  32810  zlmodzxzel  32812  zlmodzxzsubm  32816  zlmodzxzsub  32817  gsumpr  32818  scmsuppss  32835  ply1mulgsum  32860  dmatALTbas  32872  lcoop  32882  lincval0  32886  lco0  32898  linds0  32936  snlindsntorlem  32941  lmod1lem2  32959  lmod1lem3  32960  lmod1zr  32964  lmod1zrnlvec  32965  zlmodzxznm  32968  zlmodzxzldeplem4  32974  eqlkr2  34700  tendoidcl  36370  cdlemk56  36572  dihpN  36938  mapdhval  37326  hlhillcs  37563
  Copyright terms: Public domain W3C validator