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

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

Proof of Theorem mp1i
StepHypRef Expression
1 mp1i.a . . 3
2 mp1i.b . . 3
31, 2ax-mp 5 . 2
43a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  poirr2  5396  relcoi2  5540  fvrnressn  6086  isomin  6233  isoini  6234  supp0  6923  suppval1  6924  suppssr  6950  dmtpos  6986  mpt2curryd  7017  oaabs2  7313  mapsncnv  7485  boxcutc  7532  domunsncan  7637  pw2f1o  7642  unxpdom2  7748  sucxpdom  7749  findcard2d  7782  ac6sfi  7784  xpfi  7811  imafi  7833  snopfsupp  7872  fifo  7912  ordtypelem4  7967  oismo  7986  wofib  7991  brwdom2  8020  canthwdom  8026  cantnffvalOLD  8103  cantnfval  8108  cantnflt  8112  cantnff  8114  cantnf0  8115  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1  8129  cantnfltOLD  8142  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1dOLD  8151  cantnflem1OLD  8152  cnfcom  8165  cnfcom2lem  8166  cnfcomOLD  8173  cnfcom2lemOLD  8174  ranksnb  8266  tskwe  8352  cardidm  8361  infxpenc  8416  infxpencOLD  8421  fseqdom  8428  dfac8clem  8434  dfac12lem2  8545  infmap2  8619  isfin4-3  8716  fin23lem14  8734  fin23lem40  8752  isf34lem7  8780  isf34lem6  8781  fin1a2lem12  8812  hsmexlem4  8830  hsmexlem5  8831  ac5b  8879  alephexp1  8975  alephsuc3  8976  axpowndlem2OLD  8995  fpwwe2lem8  9036  fpwwe2lem13  9041  canthwe  9050  canthp1lem2  9052  gchcda1  9055  pwfseqlem5  9062  wunco  9132  prlem934  9432  supsrlem  9509  msqge0  10099  ofnegsub  10559  ofsubge0  10560  xaddpnf1  11454  supxrmnf  11538  injresinjlem  11925  uzindi  12091  seqfeq4  12156  seqof  12164  bcval5  12396  hashdomi  12448  hash1snb  12479  brfi1uzind  12532  lsw0  12586  ccatlen  12594  lswccatn0lsw  12607  s111  12623  lswccats1fst  12639  swrdspsleq  12673  wrdeqswrdlsw  12674  wrdeqs1cat  12700  reps  12742  repsw0  12749  repswccat  12757  repswrevw  12758  lswcshw  12783  cshwsexa  12792  scshwfzeqfzo  12794  wrdlen2i  12884  shftfib  12905  limsupcl  13296  limsupgf  13298  limsupval2  13303  isercolllem3  13489  modfsummods  13607  ackbijnn  13640  supcvg  13667  fprodfac  13777  ege2le3  13825  rpnnen2lem5  13952  ruclem11  13973  fsumdvds  14029  bitsinv2  14093  sadaddlem  14116  smupf  14128  smup0  14129  smu01lem  14135  isprm6  14250  hashdvds  14305  reumodprminv  14329  prmreclem6  14439  vdwlem13  14511  ramtlecl  14518  0ram  14538  cshwshashnsame  14588  prmlem0  14591  wunndx  14648  prdsval  14852  xpsbas  14971  xpsadd  14973  xpsmul  14974  xpssca  14975  xpsvsca  14976  xpsless  14977  xpsle  14978  mreexexlem2d  15042  mreacs  15055  acsfn  15056  idfu2nd  15246  idfucl  15250  fucsect  15341  setccatid  15411  setcepi  15415  catchomfval  15425  uncfval  15503  oduglb  15769  odumeet  15770  odulub  15771  odujoin  15772  isipodrs  15791  fpwipodrs  15794  isacs4lem  15798  isacs5lem  15799  idmhm  15975  submacs  15996  frmdup1  16032  mgmnsgrpex  16049  mulgneg2  16169  subgacs  16236  nsgacs  16237  idrespermg  16436  psgnunilem5  16519  psgnsn  16545  odf1o2  16593  frgpuplem  16790  cygctb  16894  gsumzunsnd  16982  gsum2dlem2  16998  gsum2dOLD  17000  gsummptnn0fz  17014  dprdsubg  17071  dmdprdsplit2lem  17094  dmdprdpr  17098  dprdpr  17099  dpjeq  17108  dpjeqOLD  17115  ablfac1eulem  17123  pgpfac1lem2  17126  pgpfaclem1  17132  srgbinomlem4  17194  unitgrp  17316  isirred  17348  brric  17393  mptscmfsupp0  17576  lssacs  17613  pwssplit1  17705  lbsextlem2  17805  lbsextlem3  17806  isnzr2hash  17912  0ring01eqbi  17921  rng1nnzr  17922  psrass1lem  18029  psrlidm  18056  psrlidmOLD  18057  resspsradd  18071  resspsrmul  18072  resspsrvsca  18073  mplcoe5lem  18130  ltbwe  18137  coe1fsupp  18254  psropprmul  18279  coe1add  18305  coe1mul2lem1  18308  coe1tm  18314  cply1coe0bi  18342  evls1rhmlem  18358  evl1sca  18370  evl1var  18372  pf1mpf  18388  pf1ind  18391  xrsmcmn  18441  xrs1mnd  18456  xrs10  18457  gsumfsum  18484  zringlpir  18512  zringcyg  18513  zlpirlem3  18516  zlpir  18517  zcyg  18518  mulgrhmOLD  18535  mulgrhm2OLD  18536  zndvds  18588  regsumsupp  18658  uvcvv1  18820  lsslinds  18866  matmulr  18940  ofco2  18953  mat0dimbas0  18968  mat1dimelbas  18973  mat1f1o  18980  dmatval  18994  scmatghm  19035  mavmul0  19054  mavmul0g  19055  m1detdiag  19099  mdetunilem9  19122  maducoeval2  19142  madugsum  19145  smadiadetlem0  19163  smadiadetlem1a  19165  smadiadetlem4  19171  smadiadetglem1  19173  smadiadetglem2  19174  smadiadetg  19175  cramer0  19192  cpmat  19210  mat2pmatfval  19224  cpm2mfval  19250  m2cpminvid2lem  19255  pmatcollpw3fi1lem2  19288  pmatcollpw3fi1  19289  idpm2idmp  19302  pm2mpmhmlem2  19320  chpmatfval  19331  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  cpmidpmatlem2  19372  cpmadugsumlemF  19377  cpmidgsum2  19380  cpmadumatpolylem1  19382  cayhamlem3  19388  cayhamlem4  19389  indistopon  19502  mreclatdemoBAD  19597  mnfnei  19722  resthauslem  19864  sshauslem  19873  discmp  19898  conima  19926  1stcfb  19946  hauseqlcld  20147  xkoptsub  20155  xkofvcn  20185  idqtop  20207  tgqtop  20213  kqdisj  20233  xpstopnlem1  20310  xpstopnlem2  20312  ufildom1  20427  alexsubb  20546  alexsubALTlem3  20549  ptcmplem2  20553  ptcmplem3  20554  tmdgsum  20594  ustneism  20726  ustuqtop1  20744  iducn  20786  prdsmet  20873  imasdsf1olem  20876  xpsxmet  20883  xpsdsval  20884  xpsmet  20885  prdsbl  20994  met1stc  21024  prdsxmslem2  21032  xpsxms  21037  xpsms  21038  psmetutop  21086  dscmet  21093  nmoffn  21218  nmofval  21221  nmolb  21224  nmof  21226  cnbl0  21281  xrsmopn  21317  xrge0gsumle  21338  xrge0tsms  21339  negfcncf  21423  cnrehmeo  21453  lebnum  21464  xlebnum  21465  reparphti  21497  pcopt  21522  pcopt2  21523  pcorevcl  21525  pcorevlem  21526  pi1xfrval  21554  pi1xfrcnvlem  21556  pi1xfrcnv  21557  pi1cof  21559  pi1coval  21560  nmhmcn  21603  cphsubrglem  21624  csscld  21689  cmetcaulem  21727  cmpcmet  21756  ovolunlem1  21908  ovolicc2lem4  21931  ioovolcl  21979  ioorcl2  21981  uniioovol  21988  uniioombllem4  21995  uniioombllem5  21996  uniioombllem6  21997  dyadmbllem  22008  mbfsub  22069  itg1climres  22121  xrge0f  22138  itg2ge0  22142  itg2i1fseq2  22163  ibl0  22193  ellimc2  22281  limcflf  22285  dvreslem  22313  dvidlem  22319  dvid  22321  cpnres  22340  dvaddbr  22341  dvmulbr  22342  dvfre  22354  dvexp  22356  dvrec  22358  dvmptid  22360  dvmptc  22361  dvmptntr  22374  dvexp3  22379  dvlipcn  22395  dveq0  22401  dv11cn  22402  lhop2  22416  ftc1a  22438  tdeglem1  22456  tdeglem3  22457  tdeglem4  22458  tdeglem2  22459  mdeg0  22470  mdegle0  22477  ply1remlem  22563  fta1glem2  22567  plypf1  22609  coe0  22653  dvply1  22680  elqaalem3  22717  aaliou2b  22737  aaliou3lem8  22741  aaliou3lem7  22745  taylfvallem  22753  taylf  22756  tayl0  22757  taylpfval  22760  taylply  22764  dvtaylp  22765  taylthlem1  22768  taylthlem2  22769  ulmdvlem1  22795  ulmdvlem2  22796  ulmdvlem3  22797  radcnvcl  22812  psercnlem2  22819  psercn  22821  pserdv  22824  abelthlem3  22828  abelth  22836  sincn  22839  coscn  22840  reefgim  22845  tangtx  22898  pige3  22910  cosordlem  22918  logcn  23028  dvlog  23032  advlog  23035  advlogexp  23036  logtayl  23041  logccv  23044  dvcxp1  23116  cxpcn3lem  23121  cxpcn3  23122  resqrtcn  23123  sqrtcn  23124  loglesqrt  23132  isosctrlem2  23153  dquartlem1  23182  quart  23192  atancj  23241  efiatan  23243  atantan  23254  atanbndlem  23256  atansopn  23263  dvatan  23266  atantayl  23268  leibpilem2  23272  leibpi  23273  log2tlbnd  23276  rlimcnp2  23296  efrlim  23299  divsqrtsumlem  23309  jensenlem1  23316  jensenlem2  23317  jensen  23318  amgmlem  23319  amgm  23320  emcllem4  23328  emcllem7  23331  wilthlem2  23343  wilthlem3  23344  basellem6  23359  chtrpcl  23449  ppiltx  23451  1sgm2ppw  23475  chtlepsi  23481  chpub  23495  logfacbnd3  23498  logfacrlim  23499  perfectlem2  23505  dchrelbas2  23512  dchrabs  23535  dchrhash  23546  bposlem7  23565  lgsdir2lem5  23602  lgsqrlem1  23616  lgseisenlem4  23627  lgsquad2lem1  23633  lgsquad3  23636  chpo1ub  23665  vmadivsumb  23668  rpvmasumlem  23672  dchrisumlem2  23675  dchrmusumlema  23678  dchrvmasumlem2  23683  dchrvmasumlema  23685  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0lem1  23701  rplogsum  23712  mudivsum  23715  logdivsum  23718  mulog2sumlem2  23720  vmalogdivsum2  23723  2vmadivsumlem  23725  log2sumbnd  23729  selberglem2  23731  selbergb  23734  selberg2lem  23735  selberg2b  23737  selberg3lem1  23742  selberg4lem1  23745  selberg4  23746  pntrsumo1  23750  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntibndlem1  23774  pntibndlem2  23776  pntibndlem3  23777  pntlemb  23782  pntlemr  23787  pntlemf  23790  pntlem3  23794  pnt  23799  qabvle  23810  padicabv  23815  ostth1  23818  istrkg2ld  23858  tgldimor  23893  motgrp  23930  perpln1  24087  perpln2  24088  isperp  24089  uhgrares  24308  umgrares  24324  edgopval  24340  usgrares  24369  nbgraop  24423  nbgraopALT  24424  nbgraf1o0  24446  cusgra0v  24460  cusgra1v  24461  cusgraexilem2  24467  sizeusglecusg  24486  isuvtx  24488  2trllemH  24554  wlkntrllem3  24563  2wlklem1  24599  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  constr3trllem3  24652  constr3pthlem3  24657  wwlkn  24682  wlkiswwlk2  24697  wwlkn0s  24705  usg2wlkeq  24708  wwlkexthasheq  24734  wlknwwlknvbij  24740  clwwlkn  24767  clwwlkn2  24775  clwlkisclwwlklem2  24786  clwwlkvbij  24801  eclclwwlkn0  24831  hashecclwwlkn1  24834  usghashecclwwlk  24835  vdgr0  24900  rusgrasn  24945  eupatrl  24968  eupares  24975  vdegp1ai  24984  vdegp1bi  24985  frgra3v  25002  frgrancvvdeqlem9  25041  frgrancvvdgeq  25043  frg2wot1  25057  usgreghash2spotv  25066  extwwlkfablem2  25078  numclwwlkovf2  25084  numclwwlk2lem3  25106  vsfval  25528  ipasslem7  25751  minvecolem2  25791  h2hcau  25896  h2hlm  25897  hlimadd  26110  hhsscms  26195  chocunii  26219  occllem  26221  leopnmid  27057  opsqrlem1  27059  hmopidmchi  27070  mdslj1i  27238  addltmulALT  27365  imadifxp  27458  xaddeq0  27573  xrge0npcan  27684  gsumle  27770  gsummpt2co  27771  xrge0tsmsd  27775  locfinreflem  27843  locfinref  27844  xpinpreima2  27889  cnre2csqlem  27892  tpr2rico  27894  ordtrestNEW  27903  ordtrest2NEW  27905  mndpluscn  27908  pnfneige0  27933  qqhghm  27969  qqhrhm  27970  qqhcn  27972  qqhucn  27973  rrhcn  27978  rrhre  27999  esumsplit  28063  esumpr  28073  esumfsup  28076  sigaclcu2  28120  pwsiga  28130  prsiga  28131  measvuni  28185  elmbfmvol2  28238  mbfmcnt  28239  sxbrsigalem1  28256  sxbrsiga  28261  omsfval  28265  sibf0  28276  sitgclg  28284  sitmval  28290  eulerpartgbij  28311  eulerpartlemgh  28317  isrrvv  28382  rrvadd  28391  rrvmulc  28392  dstrvprob  28410  coinflipspace  28419  coinfliprv  28421  ballotlemfmpn  28433  ballotlem1ri  28473  sgnmulsgn  28488  plymul02  28503  signsplypnf  28507  signsply0  28508  signswrid  28515  lgamcvg2  28597  gamcvg2lem  28601  indispcon  28679  conpcon  28680  iccllyscon  28695  cvmopnlem  28723  cvmliftlem15  28743  cvmlift2lem3  28750  mrsubff  28872  mrsubccat  28878  circum  29040  fallfac0  29150  bpoly4  29821  elhf2  29832  finixpnum  30038  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  dvtan  30065  itg2addnclem  30066  ftc1anclem5  30094  dvcncxp1  30100  dvasin  30103  dvreasin  30105  dvreacos  30106  areacirclem1  30107  areacirc  30112  bnd2lem  30287  prdsbnd  30289  cntotbnd  30292  cnpwstotbnd  30293  isdrngo2  30361  prter2  30622  isnacs3  30642  diophrw  30692  lzenom  30703  diophin  30706  pellexlem5  30769  pw2f1ocnv  30979  dnnumch2  30991  kelac2lem  31010  kelac2  31011  dfac21  31012  pwfi2f1o  31044  frlmpwfi  31046  mpaaeu  31099  rngunsnply  31122  mendbas  31133  mendplusgfval  31134  mendmulrfval  31136  mendsca  31138  mendvscafval  31139  subrgacs  31149  sdrgacs  31150  cntzsdrg  31151  idomodle  31153  phisum  31159  proot1ex  31161  deg1mhm  31167  itgpowd  31182  hashnzfzclim  31227  ofsubid  31229  ofdivrec  31231  dvconstbi  31239  fzisoeu  31500  sumnnodd  31636  negcncfg  31683  cnfdmsn  31684  divcncf  31686  dvmptresicc  31716  itgcoscmulx  31768  stoweidlem13  31795  stoweidlem26  31808  stoweidlem34  31816  stoweidlem42  31824  stoweidlem44  31826  stoweidlem48  31830  stoweidlem62  31844  stoweid  31845  stirlinglem7  31862  stirlinglem11  31866  stirlinglem12  31867  dirkeritg  31884  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem24  31913  fourierdlem48  31937  fourierdlem49  31938  fourierdlem62  31951  fourierdlem70  31959  fourierdlem80  31969  fourierdlem83  31972  fourierdlem85  31974  fourierdlem102  31991  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem114  32003  etransclem18  32035  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem35  32052  etransclem46  32063  uhgrepe  32378  uhgres  32379  gordopval  32390  gsizopval  32391  usgedgnlp  32410  isfusgracl  32426  isfusgraclALT  32428  usgo0s0  32435  usgo0s0ALT  32436  usgo1s0ALT  32437  usgo1s0  32442  usgresvm1  32443  usgfis  32446  usgresvm1ALT  32447  usgrafiedgALT  32451  idmgmhm  32476  mgmplusgiopALT  32518  sgrp2sgrp  32552  isofn  32567  ciclcl  32586  cicrcl  32587  cicsym  32588  cicer  32590  initoeu2lem1  32620  initoeu2lem2  32621  estrccatid  32638  estrreslem1  32643  estrreslem2  32644  estrres  32645  funcestrcsetclem8  32653  fullestrcsetc  32657  embedsetcestrclem  32663  funcsetcestrclem8  32668  isrnghm  32698  lidlmmgm  32731  2zrngnmlid  32755  dfrngc2  32780  rnghmsscmap2  32781  rnghmsscmap  32782  rngchomfvalOLD  32792  rngcidOLD  32799  funcrngcsetcALT  32807  dfringc2  32826  rhmsscmap2  32827  rhmsscmap  32828  rhmsscrnghm  32834  rngcresringcat  32838  funcringcsetcOLD2lem8  32851  ringchomfvalOLD  32855  ringcidOLD  32862  funcringcsetclem8OLD  32874  srhmsubc  32884  fldc  32891  rngcrescrhm  32893  rhmsubclem3  32896  srhmsubcOLD  32903  fldcOLD  32910  rngcrescrhmOLD  32912  altgsumbcALT  32942  zlmodzxzel  32944  zlmodzxzsubm  32948  zlmodzxzsub  32949  gsumpr  32950  scmsuppss  32965  ply1mulgsum  32990  dmatALTbas  33002  lcoop  33012  lincval0  33016  lco0  33028  linds0  33066  snlindsntorlem  33071  lmod1lem2  33089  lmod1lem3  33090  lmod1zr  33094  lmod1zrnlvec  33095  zlmodzxznm  33098  zlmodzxzldeplem4  33104  eqlkr2  34825  tendoidcl  36495  cdlemk56  36697  dihpN  37063  mapdhval  37451  hlhillcs  37688
This theorem was proved from axioms:  ax-mp 5  ax-1 6
  Copyright terms: Public domain W3C validator