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  |-  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 8 . 2  |-  ps
43a1i 11 1  |-  ( ch 
->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  poirr2  5249  relcoi2  5388  isomin  6048  isoini  6049  dmtpos  6482  oaabs2  6879  mapsncnv  7051  boxcutc  7096  domunsncan  7199  pw2f1o  7204  unxpdom2  7308  sucxpdom  7309  ac6sfi  7342  xpfi  7369  imafi  7390  fifo  7428  ordtypelem4  7479  oismo  7498  wofib  7503  brwdom2  7530  canthwdom  7536  cantnflt  7616  cantnff  7618  cantnf0  7619  cantnfp1lem1  7623  cantnfp1lem3  7625  cantnflem1b  7631  cantnflem1d  7633  cantnflem1  7634  cnfcom  7646  cnfcom2lem  7647  ranksnb  7742  tskwe  7826  cardidm  7835  infxpenc  7888  fseqdom  7896  dfac8clem  7902  dfac12lem2  8013  infmap2  8087  isfin4-3  8184  fin23lem14  8202  fin23lem40  8220  isf34lem7  8248  isf34lem6  8249  fin1a2lem12  8280  hsmexlem4  8298  hsmexlem5  8299  ac5b  8347  alephexp1  8443  alephsuc3  8444  axpowndlem2  8462  fpwwe2lem8  8501  fpwwe2lem13  8506  canthwe  8515  canthp1lem2  8517  gchcda1  8520  pwfseqlem5  8527  wunco  8597  prlem934  8899  supsrlem  8975  msqge0  9538  ofnegsub  9987  ofsubge0  9988  xaddpnf1  10801  supxrmnf  10885  injresinjlem  11187  uzindi  11308  seqfeq4  11360  seqof  11368  bcval5  11597  hashdomi  11642  hash1snb  11669  brfi1uzind  11703  ccatlen  11732  s111  11750  wrdeqs1cat  11777  shftfib  11875  limsupcl  12255  limsupgf  12257  limsupval2  12262  isercolllem3  12448  ackbijnn  12595  supcvg  12623  ege2le3  12680  rpnnen2lem5  12806  ruclem11  12827  fsumdvds  12881  bitsinv2  12943  sadaddlem  12966  smupf  12978  smup0  12979  smu01lem  12985  isprm6  13097  hashdvds  13152  vdwlem13  13349  ramtlecl  13356  0ram  13376  prmlem0  13416  wunndx  13473  prdsval  13666  xpsbas  13787  xpsadd  13789  xpsmul  13790  xpssca  13791  xpsvsca  13792  xpsless  13793  xpsle  13794  mreexexlem2d  13858  mreacs  13871  acsfn  13872  idfu2nd  14062  idfucl  14066  fucsect  14157  setccatid  14227  setcepi  14231  catchomfval  14241  uncfval  14319  oduglb  14554  odumeet  14555  odulub  14556  odujoin  14557  isipodrs  14575  fpwipodrs  14578  isacs4lem  14582  isacs5lem  14583  submacs  14753  frmdup1  14797  mulgneg2  14905  subgacs  14963  nsgacs  14964  odf1o2  15195  frgpuplem  15392  cygctb  15489  gsum2d  15534  dprdsubg  15570  dmdprdsplit2lem  15591  dmdprdpr  15595  dprdpr  15596  dpjeq  15605  ablfac1eulem  15618  pgpfac1lem2  15621  pgpfaclem1  15627  unitgrp  15760  isirred  15792  lssacs  16031  lbsextlem2  16219  lbsextlem3  16220  psrlidm  16455  resspsradd  16467  resspsrmul  16468  resspsrvsca  16469  ltbwe  16521  coe1add  16645  coe1mul2lem1  16648  coe1tm  16653  xrsmcmn  16712  xrs1mnd  16724  xrs10  16725  gsumfsum  16754  zlpirlem3  16758  zlpir  16759  zcyg  16760  mulgrhm  16775  mulgrhm2  16776  zlmlmod  16792  zlmassa  16793  znbas  16812  znzrhfo  16816  zndvds  16818  frgpcyg  16842  indistopon  17053  mreclatdemo  17148  mnfnei  17273  resthauslem  17415  sshauslem  17424  discmp  17449  conima  17476  1stcfb  17496  hauseqlcld  17666  xkoptsub  17674  xkofvcn  17704  idqtop  17726  tgqtop  17732  kqdisj  17752  xpstopnlem1  17829  xpstopnlem2  17831  ufildom1  17946  alexsubb  18065  alexsubALTlem3  18068  ptcmplem2  18072  ptcmplem3  18073  tmdgsum  18113  ustneism  18241  ustuqtop1  18259  iducn  18301  prdsmet  18388  imasdsf1olem  18391  xpsxmet  18398  xpsdsval  18399  xpsmet  18400  prdsbl  18509  met1stc  18539  prdsxmslem2  18547  xpsxms  18552  xpsms  18553  dscmet  18608  nmoffn  18733  nmofval  18736  nmolb  18739  nmof  18741  cnbl0  18796  xrsmopn  18831  xrge0gsumle  18852  xrge0tsms  18853  negfcncf  18937  cnrehmeo  18966  lebnum  18977  xlebnum  18978  reparphti  19010  pcopt  19035  pcopt2  19036  pcorevcl  19038  pcorevlem  19039  pi1xfrval  19067  pi1xfrcnvlem  19069  pi1xfrcnv  19070  pi1cof  19072  pi1coval  19073  nmhmcn  19116  cphsubrglem  19128  csscld  19191  cmetcaulem  19229  cmpcmet  19258  ovolunlem1  19381  ovolicc2lem4  19404  ioorcl2  19452  uniioovol  19459  uniioombllem4  19466  uniioombllem5  19467  uniioombllem6  19468  dyadmbllem  19479  mbfsub  19542  itg1climres  19594  xrge0f  19611  itg2ge0  19615  itg2i1fseq2  19636  ibl0  19666  ellimc2  19752  limcflf  19756  dvreslem  19784  dvidlem  19790  dvid  19792  cpnres  19811  dvaddbr  19812  dvmulbr  19813  dvfre  19825  dvexp  19827  dvrec  19829  dvmptid  19831  dvmptc  19832  dvmptntr  19845  dvexp3  19850  dvlipcn  19866  dveq0  19872  dv11cn  19873  lhop2  19887  ftc1a  19909  evl1rhm  19937  evl1sca  19938  evl1var  19940  pf1mpf  19960  pf1ind  19963  tdeglem1  19969  tdeglem3  19970  tdeglem4  19971  tdeglem2  19972  mdegle0  19988  ply1remlem  20073  fta1glem2  20077  plypf1  20119  coe0  20162  dvply1  20189  elqaalem3  20226  aaliou2b  20246  aaliou3lem8  20250  aaliou3lem7  20254  taylfvallem  20262  taylf  20265  tayl0  20266  taylpfval  20269  taylply  20273  dvtaylp  20274  taylthlem1  20277  taylthlem2  20278  ulmdvlem1  20304  ulmdvlem2  20305  ulmdvlem3  20306  radcnvcl  20321  psercnlem2  20328  psercn  20330  pserdv  20333  abelthlem3  20337  abelth  20345  sincn  20348  coscn  20349  reefgim  20354  tangtx  20401  pige3  20413  cosordlem  20421  logcn  20526  dvlog  20530  advlog  20533  advlogexp  20534  logtayl  20539  logccv  20542  dvcxp1  20614  cxpcn3lem  20619  cxpcn3  20620  resqrcn  20621  sqrcn  20622  loglesqr  20630  isosctrlem2  20651  dquartlem1  20679  quart  20689  atancj  20738  efiatan  20740  atantan  20751  atanbndlem  20753  atansopn  20760  dvatan  20763  atantayl  20765  leibpilem2  20769  leibpi  20770  log2tlbnd  20773  rlimcnp2  20793  efrlim  20796  divsqrsumlem  20806  jensenlem1  20813  jensenlem2  20814  jensen  20815  amgmlem  20816  amgm  20817  emcllem4  20825  emcllem7  20828  wilthlem2  20840  wilthlem3  20841  basellem6  20856  chtrpcl  20946  ppiltx  20948  1sgm2ppw  20972  chtlepsi  20978  chpub  20992  logfacbnd3  20995  logfacrlim  20996  perfectlem2  21002  dchrelbas2  21009  dchrabs  21032  dchrhash  21043  bposlem7  21062  lgsdir2lem5  21099  lgsqrlem1  21113  lgseisenlem4  21124  lgsquad2lem1  21130  lgsquad3  21133  chpo1ub  21162  vmadivsumb  21165  rpvmasumlem  21169  dchrisumlem2  21172  dchrmusumlema  21175  dchrvmasumlem2  21180  dchrvmasumlema  21182  dchrvmasumiflem1  21183  dchrisum0flblem1  21190  dchrisum0lem1  21198  rplogsum  21209  mudivsum  21212  logdivsum  21215  mulog2sumlem2  21217  vmalogdivsum2  21220  2vmadivsumlem  21222  log2sumbnd  21226  selberglem2  21228  selbergb  21231  selberg2lem  21232  selberg2b  21234  selberg3lem1  21239  selberg4lem1  21242  selberg4  21243  pntrsumo1  21247  pntrlog2bndlem2  21260  pntrlog2bndlem3  21261  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  pntibndlem1  21271  pntibndlem2  21273  pntibndlem3  21274  pntlemb  21279  pntlemr  21284  pntlemf  21287  pntlem3  21291  pnt  21296  qabvle  21307  padicabv  21312  ostth1  21315  uhgrares  21331  umgrares  21347  usgrares  21377  nbgraop  21424  nbgraf1o0  21444  cusgra0v  21457  cusgra1v  21458  cusgraexilem2  21464  sizeusglecusg  21483  isuvtx  21485  2trllemH  21540  wlkntrllem3  21549  2wlklem1  21585  constr3trllem3  21627  constr3pthlem3  21632  vdgr0  21659  eupatrl  21678  eupares  21685  vdegp1ai  21694  vdegp1bi  21695  vsfval  22102  ipasslem7  22325  minvecolem2  22365  h2hcau  22470  h2hlm  22471  hlimadd  22683  hhsscms  22767  chocunii  22791  occllem  22793  leopnmid  23629  opsqrlem1  23631  hmopidmchi  23642  mdslj1i  23810  addltmulALT  23937  imadifxp  24026  xaddeq0  24107  xrge0npcan  24204  xrge0tsmsd  24211  xpinpreima2  24293  cnre2csqlem  24296  tpr2rico  24298  mndpluscn  24300  pnfneige0  24324  qqhghm  24360  qqhrhm  24361  qqhcn  24363  qqhucn  24364  esumsplit  24435  esumpr  24445  esumfsup  24448  sigaclcu2  24491  pwsiga  24501  prsiga  24502  measvuni  24556  elmbfmvol2  24605  mbfmcnt  24606  sxbrsigalem1  24623  sxbrsiga  24628  sibf0  24637  sitgclg  24644  isrrvv  24689  rrvadd  24698  rrvmulc  24699  dstrvprob  24717  coinflipspace  24726  coinfliprv  24728  ballotlemfmpn  24740  ballotlem1ri  24780  lgamcvg2  24827  gamcvg2lem  24831  indispcon  24909  conpcon  24910  iccllyscon  24925  cvmopnlem  24953  cvmliftlem15  24973  cvmlift2lem3  24980  circum  25099  fprodfac  25285  fallfac0  25333  bpoly4  26053  elhf2  26064  mblfinlem  26190  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  ovoliunnfl  26194  voliunnfl  26196  volsupnfl  26197  itg2addnclem  26202  dvreasin  26226  dvreacos  26227  areacirclem2  26228  areacirclem3  26229  bnd2lem  26437  prdsbnd  26439  cntotbnd  26442  cnpwstotbnd  26443  isdrngo2  26511  prter2  26667  isnacs3  26701  diophrw  26754  lzenom  26765  diophin  26768  pellexlem5  26833  pw2f1ocnv  27045  dnnumch2  27057  kelac2lem  27077  kelac2  27078  dfac21  27079  pwssplit1  27103  uvcvv1  27153  pwfi2f1o  27175  frlmpwfi  27177  lsslinds  27216  mpaaeu  27270  rngunsnply  27293  psgnunilem5  27332  matmulr  27382  mendbas  27407  mendplusgfval  27408  mendmulrfval  27410  mendsca  27412  mendvscafval  27413  subrgacs  27423  sdrgacs  27424  cntzsdrg  27425  idomodle  27427  phisum  27433  proot1ex  27435  deg1mhm  27441  ofsubid  27456  ofdivrec  27458  dvconstbi  27466  ioovolcl  27656  stoweidlem13  27676  stoweidlem26  27689  stoweidlem34  27697  stoweidlem42  27705  stoweidlem44  27707  stoweidlem48  27711  stoweidlem62  27725  stoweid  27726  stirlinglem7  27743  stirlinglem11  27747  reumodprminv  28111  shwrdoor  28125  lswrd0  28150  lswrdshwrd  28152  shwrdssizelem1a  28165  shwrdssizensame  28174  usgra2wlkspthlem1  28180  usgra2wlkspthlem2  28181  frgra3v  28250  frgrancvvdeqlem9  28288  frgrancvvdgeq  28290  frg2wot1  28304  usgreghash2spotv  28313  eqlkr2  29737  tendoidcl  31405  cdlemk56  31607  dihpN  31973  mapdhval  32361  hlhillcs  32598
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator