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  5389  relcoi2  5533  fvrnressn  6074  isomin  6219  isoini  6220  supp0  6903  suppval1  6904  suppssr  6928  dmtpos  6964  mpt2curryd  6995  oaabs2  7291  mapsncnv  7462  boxcutc  7509  domunsncan  7614  pw2f1o  7619  unxpdom2  7725  sucxpdom  7726  findcard2d  7758  ac6sfi  7760  xpfi  7787  imafi  7809  snopfsupp  7848  fifo  7888  ordtypelem4  7942  oismo  7961  wofib  7966  brwdom2  7995  canthwdom  8001  cantnffvalOLD  8078  cantnfval  8083  cantnflt  8087  cantnff  8089  cantnf0  8090  cantnfp1lem1  8093  cantnfp1lem3  8095  cantnflem1b  8101  cantnflem1  8104  cantnfltOLD  8117  cantnfp1lem1OLD  8119  cantnfp1lem3OLD  8121  cantnflem1bOLD  8124  cantnflem1dOLD  8126  cantnflem1OLD  8127  cnfcom  8140  cnfcom2lem  8141  cnfcomOLD  8148  cnfcom2lemOLD  8149  ranksnb  8241  tskwe  8327  cardidm  8336  infxpenc  8391  infxpencOLD  8396  fseqdom  8403  dfac8clem  8409  dfac12lem2  8520  infmap2  8594  isfin4-3  8691  fin23lem14  8709  fin23lem40  8727  isf34lem7  8755  isf34lem6  8756  fin1a2lem12  8787  hsmexlem4  8805  hsmexlem5  8806  ac5b  8854  alephexp1  8950  alephsuc3  8951  axpowndlem2OLD  8970  fpwwe2lem8  9011  fpwwe2lem13  9016  canthwe  9025  canthp1lem2  9027  gchcda1  9030  pwfseqlem5  9037  wunco  9107  prlem934  9407  supsrlem  9484  msqge0  10070  ofnegsub  10530  ofsubge0  10531  xaddpnf1  11421  supxrmnf  11505  injresinjlem  11889  uzindi  12054  seqfeq4  12119  seqof  12127  bcval5  12358  hashdomi  12410  hash1snb  12438  brfi1uzind  12492  lsw0  12545  ccatlen  12553  lswccatn0lsw  12565  s111  12580  lswccats1fst  12596  swrdspsleq  12630  wrdeqswrdlsw  12631  wrdeqs1cat  12657  reps  12699  repsw0  12706  repswccat  12714  repswrevw  12715  lswcshw  12740  cshwsexa  12749  scshwfzeqfzo  12751  wrdlen2i  12841  shftfib  12862  limsupcl  13252  limsupgf  13254  limsupval2  13259  isercolllem3  13445  modfsummods  13563  ackbijnn  13596  supcvg  13623  ege2le3  13680  rpnnen2lem5  13806  ruclem11  13827  fsumdvds  13881  bitsinv2  13945  sadaddlem  13968  smupf  13980  smup0  13981  smu01lem  13987  isprm6  14102  hashdvds  14157  reumodprminv  14181  vdwlem13  14363  ramtlecl  14370  0ram  14390  cshwshashnsame  14439  prmlem0  14442  wunndx  14499  prdsval  14703  xpsbas  14822  xpsadd  14824  xpsmul  14825  xpssca  14826  xpsvsca  14827  xpsless  14828  xpsle  14829  mreexexlem2d  14893  mreacs  14906  acsfn  14907  idfu2nd  15097  idfucl  15101  fucsect  15192  setccatid  15262  setcepi  15266  catchomfval  15276  uncfval  15354  oduglb  15619  odumeet  15620  odulub  15621  odujoin  15622  isipodrs  15641  fpwipodrs  15644  isacs4lem  15648  isacs5lem  15649  submacs  15803  frmdup1  15852  mulgneg2  15966  subgacs  16028  nsgacs  16029  idrespermg  16228  psgnunilem5  16312  psgnsn  16338  odf1o2  16386  frgpuplem  16583  cygctb  16682  gsumzunsnd  16770  gsum2dlem2  16786  gsum2dOLD  16788  gsummptnn0fz  16802  dprdsubg  16858  dmdprdsplit2lem  16881  dmdprdpr  16885  dprdpr  16886  dpjeq  16895  dpjeqOLD  16902  ablfac1eulem  16910  pgpfac1lem2  16913  pgpfaclem1  16919  srgbinomlem4  16979  unitgrp  17097  isirred  17129  brric  17173  mptscmfsupp0  17356  lssacs  17393  pwssplit1  17485  lbsextlem2  17585  lbsextlem3  17586  psrass1lem  17797  psrlidm  17824  psrlidmOLD  17825  resspsradd  17839  resspsrmul  17840  resspsrvsca  17841  mplcoe5lem  17898  ltbwe  17905  coe1fsupp  18022  psropprmul  18047  coe1add  18073  coe1mul2lem1  18076  coe1tm  18082  evls1rhmlem  18126  evl1sca  18138  evl1var  18140  pf1mpf  18156  pf1ind  18159  xrsmcmn  18209  xrs1mnd  18221  xrs10  18222  gsumfsum  18249  zringlpir  18276  zringcyg  18277  zlpirlem3  18280  zlpir  18281  zcyg  18282  mulgrhmOLD  18299  mulgrhm2OLD  18300  zndvds  18352  regsumsupp  18422  uvcvv1  18584  lsslinds  18630  matmulr  18704  ofco2  18717  mat0dimbas0  18732  mat1dimelbas  18737  mat1f1o  18744  dmatval  18758  scmatghm  18799  mavmul0  18818  mavmul0g  18819  m1detdiag  18863  mdetunilem9  18886  maducoeval2  18906  madugsum  18909  smadiadetlem0  18927  smadiadetlem1a  18929  smadiadetlem4  18935  smadiadetglem1  18937  smadiadetglem2  18938  smadiadetg  18939  cramer0  18956  cpmat  18974  mat2pmatfval  18988  cpm2mfval  19014  m2cpminvid2lem  19019  pmatcollpw3fi1lem2  19052  pmatcollpw3fi1  19053  idpm2idmp  19066  pm2mpmhmlem2  19084  chpmatfval  19095  chfacfscmulfsupp  19124  chfacfpmmulfsupp  19128  cpmidpmatlem2  19136  cpmadugsumlemF  19141  cpmadumatpolylem1  19146  cayhamlem3  19152  cayhamlem4  19153  indistopon  19265  mreclatdemoBAD  19360  mnfnei  19485  resthauslem  19627  sshauslem  19636  discmp  19661  conima  19689  1stcfb  19709  hauseqlcld  19879  xkoptsub  19887  xkofvcn  19917  idqtop  19939  tgqtop  19945  kqdisj  19965  xpstopnlem1  20042  xpstopnlem2  20044  ufildom1  20159  alexsubb  20278  alexsubALTlem3  20281  ptcmplem2  20285  ptcmplem3  20286  tmdgsum  20326  ustneism  20458  ustuqtop1  20476  iducn  20518  prdsmet  20605  imasdsf1olem  20608  xpsxmet  20615  xpsdsval  20616  xpsmet  20617  prdsbl  20726  met1stc  20756  prdsxmslem2  20764  xpsxms  20769  xpsms  20770  dscmet  20825  nmoffn  20950  nmofval  20953  nmolb  20956  nmof  20958  cnbl0  21013  xrsmopn  21049  xrge0gsumle  21070  xrge0tsms  21071  negfcncf  21155  cnrehmeo  21185  lebnum  21196  xlebnum  21197  reparphti  21229  pcopt  21254  pcopt2  21255  pcorevcl  21257  pcorevlem  21258  pi1xfrval  21286  pi1xfrcnvlem  21288  pi1xfrcnv  21289  pi1cof  21291  pi1coval  21292  nmhmcn  21335  cphsubrglem  21356  csscld  21421  cmetcaulem  21459  cmpcmet  21488  ovolunlem1  21640  ovolicc2lem4  21663  ioovolcl  21711  ioorcl2  21713  uniioovol  21720  uniioombllem4  21727  uniioombllem5  21728  uniioombllem6  21729  dyadmbllem  21740  mbfsub  21801  itg1climres  21853  xrge0f  21870  itg2ge0  21874  itg2i1fseq2  21895  ibl0  21925  ellimc2  22013  limcflf  22017  dvreslem  22045  dvidlem  22051  dvid  22053  cpnres  22072  dvaddbr  22073  dvmulbr  22074  dvfre  22086  dvexp  22088  dvrec  22090  dvmptid  22092  dvmptc  22093  dvmptntr  22106  dvexp3  22111  dvlipcn  22127  dveq0  22133  dv11cn  22134  lhop2  22148  ftc1a  22170  tdeglem1  22188  tdeglem3  22189  tdeglem4  22190  tdeglem2  22191  mdeg0  22202  mdegle0  22209  ply1remlem  22295  fta1glem2  22299  plypf1  22341  coe0  22384  dvply1  22411  elqaalem3  22448  aaliou2b  22468  aaliou3lem8  22472  aaliou3lem7  22476  taylfvallem  22484  taylf  22487  tayl0  22488  taylpfval  22491  taylply  22495  dvtaylp  22496  taylthlem1  22499  taylthlem2  22500  ulmdvlem1  22526  ulmdvlem2  22527  ulmdvlem3  22528  radcnvcl  22543  psercnlem2  22550  psercn  22552  pserdv  22555  abelthlem3  22559  abelth  22567  sincn  22570  coscn  22571  reefgim  22576  tangtx  22628  pige3  22640  cosordlem  22648  logcn  22753  dvlog  22757  advlog  22760  advlogexp  22761  logtayl  22766  logccv  22769  dvcxp1  22841  cxpcn3lem  22846  cxpcn3  22847  resqrtcn  22848  sqrtcn  22849  loglesqrt  22857  isosctrlem2  22878  dquartlem1  22907  quart  22917  atancj  22966  efiatan  22968  atantan  22979  atanbndlem  22981  atansopn  22988  dvatan  22991  atantayl  22993  leibpilem2  22997  leibpi  22998  log2tlbnd  23001  rlimcnp2  23021  efrlim  23024  divsqrtsumlem  23034  jensenlem1  23041  jensenlem2  23042  jensen  23043  amgmlem  23044  amgm  23045  emcllem4  23053  emcllem7  23056  wilthlem2  23068  wilthlem3  23069  basellem6  23084  chtrpcl  23174  ppiltx  23176  1sgm2ppw  23200  chtlepsi  23206  chpub  23220  logfacbnd3  23223  logfacrlim  23224  perfectlem2  23230  dchrelbas2  23237  dchrabs  23260  dchrhash  23271  bposlem7  23290  lgsdir2lem5  23327  lgsqrlem1  23341  lgseisenlem4  23352  lgsquad2lem1  23358  lgsquad3  23361  chpo1ub  23390  vmadivsumb  23393  rpvmasumlem  23397  dchrisumlem2  23400  dchrmusumlema  23403  dchrvmasumlem2  23408  dchrvmasumlema  23410  dchrvmasumiflem1  23411  dchrisum0flblem1  23418  dchrisum0lem1  23426  rplogsum  23437  mudivsum  23440  logdivsum  23443  mulog2sumlem2  23445  vmalogdivsum2  23448  2vmadivsumlem  23450  log2sumbnd  23454  selberglem2  23456  selbergb  23459  selberg2lem  23460  selberg2b  23462  selberg3lem1  23467  selberg4lem1  23470  selberg4  23471  pntrsumo1  23475  pntrlog2bndlem2  23488  pntrlog2bndlem3  23489  pntrlog2bndlem4  23490  pntrlog2bndlem5  23491  pntibndlem1  23499  pntibndlem2  23501  pntibndlem3  23502  pntlemb  23507  pntlemr  23512  pntlemf  23515  pntlem3  23519  pnt  23524  qabvle  23535  padicabv  23540  ostth1  23543  istrkg2ld  23583  perpln1  23792  perpln2  23793  isperp  23794  uhgrares  23981  umgrares  23997  edgopval  24013  usgrares  24042  nbgraop  24096  nbgraopALT  24097  nbgraf1o0  24119  cusgra0v  24133  cusgra1v  24134  cusgraexilem2  24140  sizeusglecusg  24159  isuvtx  24161  2trllemH  24227  wlkntrllem3  24236  2wlklem1  24272  usgra2wlkspthlem1  24292  usgra2wlkspthlem2  24293  constr3trllem3  24325  constr3pthlem3  24330  wwlkn  24355  wlkiswwlk2  24370  wwlkn0s  24378  usg2wlkeq  24381  wwlkexthasheq  24407  wlknwwlknvbij  24413  clwwlkn  24440  clwwlkn2  24448  clwlkisclwwlklem2  24459  clwwlkvbij  24474  eclclwwlkn0  24504  hashecclwwlkn1  24507  usghashecclwwlk  24508  vdgr0  24573  rusgrasn  24618  eupatrl  24641  eupares  24648  vdegp1ai  24657  vdegp1bi  24658  frgra3v  24675  frgrancvvdeqlem9  24715  frgrancvvdgeq  24717  frg2wot1  24731  usgreghash2spotv  24740  extwwlkfablem2  24752  numclwwlkovf2  24758  numclwwlk2lem3  24780  vsfval  25201  ipasslem7  25424  minvecolem2  25464  h2hcau  25569  h2hlm  25570  hlimadd  25783  hhsscms  25868  chocunii  25892  occllem  25894  leopnmid  26730  opsqrlem1  26732  hmopidmchi  26743  mdslj1i  26911  addltmulALT  27038  imadifxp  27128  xaddeq0  27238  xrge0npcan  27343  gsumle  27430  xrge0tsmsd  27435  xpinpreima2  27522  cnre2csqlem  27525  tpr2rico  27527  ordtrestNEW  27536  mndpluscn  27541  pnfneige0  27566  qqhghm  27602  qqhrhm  27603  qqhcn  27605  qqhucn  27606  rrhre  27632  esumsplit  27700  esumpr  27710  esumfsup  27713  sigaclcu2  27757  pwsiga  27767  prsiga  27768  measvuni  27822  elmbfmvol2  27875  mbfmcnt  27876  sxbrsigalem1  27893  sxbrsiga  27898  omsfval  27902  sibf0  27913  sitgclg  27921  eulerpartgbij  27948  eulerpartlemgh  27954  isrrvv  28019  rrvadd  28028  rrvmulc  28029  dstrvprob  28047  coinflipspace  28056  coinfliprv  28058  ballotlemfmpn  28070  ballotlem1ri  28110  signsplypnf  28144  signsply0  28145  signswrid  28152  lgamcvg2  28234  gamcvg2lem  28238  indispcon  28316  conpcon  28317  iccllyscon  28332  cvmopnlem  28360  cvmliftlem15  28380  cvmlift2lem3  28387  circum  28512  fprodfac  28676  fallfac0  28724  bpoly4  29395  elhf2  29406  finixpnum  29612  mblfinlem3  29628  mblfinlem4  29629  ismblfin  29630  ovoliunnfl  29631  voliunnfl  29633  volsupnfl  29634  dvtan  29640  itg2addnclem  29641  ftc1anclem5  29669  dvcncxp1  29675  dvasin  29678  dvreasin  29680  dvreacos  29681  areacirclem1  29682  areacirc  29687  bnd2lem  29888  prdsbnd  29890  cntotbnd  29893  cnpwstotbnd  29894  isdrngo2  29962  prter2  30224  isnacs3  30244  diophrw  30294  lzenom  30305  diophin  30308  pellexlem5  30371  pw2f1ocnv  30583  dnnumch2  30595  kelac2lem  30614  kelac2  30615  dfac21  30616  pwfi2f1o  30648  frlmpwfi  30650  mpaaeu  30704  rngunsnply  30727  mendbas  30738  mendplusgfval  30739  mendmulrfval  30741  mendsca  30743  mendvscafval  30744  subrgacs  30754  sdrgacs  30755  cntzsdrg  30756  idomodle  30758  phisum  30764  proot1ex  30766  deg1mhm  30772  itgpowd  30787  hashnzfzclim  30827  ofsubid  30829  ofdivrec  30831  dvconstbi  30839  stoweidlem13  31313  stoweidlem26  31326  stoweidlem34  31334  stoweidlem42  31342  stoweidlem44  31344  stoweidlem48  31348  stoweidlem62  31362  stoweid  31363  stirlinglem7  31380  stirlinglem11  31384  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem42  31449  fourierdlem111  31518  uhgrepe  31847  uhgres  31848  gordopval  31859  gsizopval  31860  usgedgnlp  31879  isfusgracl  31895  isfusgraclALT  31897  usgo0s0  31904  usgo0s0ALT  31905  usgo1s0ALT  31906  usgo1s0  31911  usgresvm1  31912  usgfis  31915  usgresvm1ALT  31916  usgrafiedgALT  31920  sgrp2sgrp  31978  altgsumbcALT  32006  zlmodzxzel  32008  zlmodzxzsubm  32012  zlmodzxzsub  32013  gsumpr  32014  isnzr2hash  32027  scmsuppss  32038  ply1mulgsum  32063  dmatALTbas  32075  lcoop  32085  lincval0  32089  lco0  32101  linds0  32139  snlindsntorlem  32144  rng1nnzr  32166  lmod1lem2  32170  lmod1lem3  32171  lmod1zr  32175  lmod1zrnlvec  32176  zlmodzxznm  32179  zlmodzxzldeplem4  32185  eqlkr2  33897  tendoidcl  35565  cdlemk56  35767  dihpN  36133  mapdhval  36521  hlhillcs  36758
  Copyright terms: Public domain W3C validator