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 8 . 2  |-  ps
43a1i 11 1  |-  ( ch 
->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  poirr2  5258  relcoi2  5397  isomin  6057  isoini  6058  dmtpos  6491  oaabs2  6888  mapsncnv  7060  boxcutc  7105  domunsncan  7208  pw2f1o  7213  unxpdom2  7317  sucxpdom  7318  ac6sfi  7351  xpfi  7378  imafi  7399  fifo  7437  ordtypelem4  7490  oismo  7509  wofib  7514  brwdom2  7541  canthwdom  7547  cantnflt  7627  cantnff  7629  cantnf0  7630  cantnfp1lem1  7634  cantnfp1lem3  7636  cantnflem1b  7642  cantnflem1d  7644  cantnflem1  7645  cnfcom  7657  cnfcom2lem  7658  ranksnb  7753  tskwe  7837  cardidm  7846  infxpenc  7899  fseqdom  7907  dfac8clem  7913  dfac12lem2  8024  infmap2  8098  isfin4-3  8195  fin23lem14  8213  fin23lem40  8231  isf34lem7  8259  isf34lem6  8260  fin1a2lem12  8291  hsmexlem4  8309  hsmexlem5  8310  ac5b  8358  alephexp1  8454  alephsuc3  8455  axpowndlem2  8473  fpwwe2lem8  8512  fpwwe2lem13  8517  canthwe  8526  canthp1lem2  8528  gchcda1  8531  pwfseqlem5  8538  wunco  8608  prlem934  8910  supsrlem  8986  msqge0  9549  ofnegsub  9998  ofsubge0  9999  xaddpnf1  10812  supxrmnf  10896  injresinjlem  11199  uzindi  11320  seqfeq4  11372  seqof  11380  bcval5  11609  hashdomi  11654  hash1snb  11681  brfi1uzind  11715  ccatlen  11744  s111  11762  wrdeqs1cat  11789  shftfib  11887  limsupcl  12267  limsupgf  12269  limsupval2  12274  isercolllem3  12460  ackbijnn  12607  supcvg  12635  ege2le3  12692  rpnnen2lem5  12818  ruclem11  12839  fsumdvds  12893  bitsinv2  12955  sadaddlem  12978  smupf  12990  smup0  12991  smu01lem  12997  isprm6  13109  hashdvds  13164  vdwlem13  13361  ramtlecl  13368  0ram  13388  prmlem0  13428  wunndx  13485  prdsval  13678  xpsbas  13799  xpsadd  13801  xpsmul  13802  xpssca  13803  xpsvsca  13804  xpsless  13805  xpsle  13806  mreexexlem2d  13870  mreacs  13883  acsfn  13884  idfu2nd  14074  idfucl  14078  fucsect  14169  setccatid  14239  setcepi  14243  catchomfval  14253  uncfval  14331  oduglb  14566  odumeet  14567  odulub  14568  odujoin  14569  isipodrs  14587  fpwipodrs  14590  isacs4lem  14594  isacs5lem  14595  submacs  14765  frmdup1  14809  mulgneg2  14917  subgacs  14975  nsgacs  14976  odf1o2  15207  frgpuplem  15404  cygctb  15501  gsum2d  15546  dprdsubg  15582  dmdprdsplit2lem  15603  dmdprdpr  15607  dprdpr  15608  dpjeq  15617  ablfac1eulem  15630  pgpfac1lem2  15633  pgpfaclem1  15639  unitgrp  15772  isirred  15804  lssacs  16043  lbsextlem2  16231  lbsextlem3  16232  psrlidm  16467  resspsradd  16479  resspsrmul  16480  resspsrvsca  16481  ltbwe  16533  coe1add  16657  coe1mul2lem1  16660  coe1tm  16665  xrsmcmn  16724  xrs1mnd  16736  xrs10  16737  gsumfsum  16766  zlpirlem3  16770  zlpir  16771  zcyg  16772  mulgrhm  16787  mulgrhm2  16788  zlmlmod  16804  zlmassa  16805  znbas  16824  znzrhfo  16828  zndvds  16830  frgpcyg  16854  indistopon  17065  mreclatdemo  17160  mnfnei  17285  resthauslem  17427  sshauslem  17436  discmp  17461  conima  17488  1stcfb  17508  hauseqlcld  17678  xkoptsub  17686  xkofvcn  17716  idqtop  17738  tgqtop  17744  kqdisj  17764  xpstopnlem1  17841  xpstopnlem2  17843  ufildom1  17958  alexsubb  18077  alexsubALTlem3  18080  ptcmplem2  18084  ptcmplem3  18085  tmdgsum  18125  ustneism  18253  ustuqtop1  18271  iducn  18313  prdsmet  18400  imasdsf1olem  18403  xpsxmet  18410  xpsdsval  18411  xpsmet  18412  prdsbl  18521  met1stc  18551  prdsxmslem2  18559  xpsxms  18564  xpsms  18565  dscmet  18620  nmoffn  18745  nmofval  18748  nmolb  18751  nmof  18753  cnbl0  18808  xrsmopn  18843  xrge0gsumle  18864  xrge0tsms  18865  negfcncf  18949  cnrehmeo  18978  lebnum  18989  xlebnum  18990  reparphti  19022  pcopt  19047  pcopt2  19048  pcorevcl  19050  pcorevlem  19051  pi1xfrval  19079  pi1xfrcnvlem  19081  pi1xfrcnv  19082  pi1cof  19084  pi1coval  19085  nmhmcn  19128  cphsubrglem  19140  csscld  19203  cmetcaulem  19241  cmpcmet  19270  ovolunlem1  19393  ovolicc2lem4  19416  ioorcl2  19464  uniioovol  19471  uniioombllem4  19478  uniioombllem5  19479  uniioombllem6  19480  dyadmbllem  19491  mbfsub  19554  itg1climres  19606  xrge0f  19623  itg2ge0  19627  itg2i1fseq2  19648  ibl0  19678  ellimc2  19764  limcflf  19768  dvreslem  19796  dvidlem  19802  dvid  19804  cpnres  19823  dvaddbr  19824  dvmulbr  19825  dvfre  19837  dvexp  19839  dvrec  19841  dvmptid  19843  dvmptc  19844  dvmptntr  19857  dvexp3  19862  dvlipcn  19878  dveq0  19884  dv11cn  19885  lhop2  19899  ftc1a  19921  evl1rhm  19949  evl1sca  19950  evl1var  19952  pf1mpf  19972  pf1ind  19975  tdeglem1  19981  tdeglem3  19982  tdeglem4  19983  tdeglem2  19984  mdegle0  20000  ply1remlem  20085  fta1glem2  20089  plypf1  20131  coe0  20174  dvply1  20201  elqaalem3  20238  aaliou2b  20258  aaliou3lem8  20262  aaliou3lem7  20266  taylfvallem  20274  taylf  20277  tayl0  20278  taylpfval  20281  taylply  20285  dvtaylp  20286  taylthlem1  20289  taylthlem2  20290  ulmdvlem1  20316  ulmdvlem2  20317  ulmdvlem3  20318  radcnvcl  20333  psercnlem2  20340  psercn  20342  pserdv  20345  abelthlem3  20349  abelth  20357  sincn  20360  coscn  20361  reefgim  20366  tangtx  20413  pige3  20425  cosordlem  20433  logcn  20538  dvlog  20542  advlog  20545  advlogexp  20546  logtayl  20551  logccv  20554  dvcxp1  20626  cxpcn3lem  20631  cxpcn3  20632  resqrcn  20633  sqrcn  20634  loglesqr  20642  isosctrlem2  20663  dquartlem1  20691  quart  20701  atancj  20750  efiatan  20752  atantan  20763  atanbndlem  20765  atansopn  20772  dvatan  20775  atantayl  20777  leibpilem2  20781  leibpi  20782  log2tlbnd  20785  rlimcnp2  20805  efrlim  20808  divsqrsumlem  20818  jensenlem1  20825  jensenlem2  20826  jensen  20827  amgmlem  20828  amgm  20829  emcllem4  20837  emcllem7  20840  wilthlem2  20852  wilthlem3  20853  basellem6  20868  chtrpcl  20958  ppiltx  20960  1sgm2ppw  20984  chtlepsi  20990  chpub  21004  logfacbnd3  21007  logfacrlim  21008  perfectlem2  21014  dchrelbas2  21021  dchrabs  21044  dchrhash  21055  bposlem7  21074  lgsdir2lem5  21111  lgsqrlem1  21125  lgseisenlem4  21136  lgsquad2lem1  21142  lgsquad3  21145  chpo1ub  21174  vmadivsumb  21177  rpvmasumlem  21181  dchrisumlem2  21184  dchrmusumlema  21187  dchrvmasumlem2  21192  dchrvmasumlema  21194  dchrvmasumiflem1  21195  dchrisum0flblem1  21202  dchrisum0lem1  21210  rplogsum  21221  mudivsum  21224  logdivsum  21227  mulog2sumlem2  21229  vmalogdivsum2  21232  2vmadivsumlem  21234  log2sumbnd  21238  selberglem2  21240  selbergb  21243  selberg2lem  21244  selberg2b  21246  selberg3lem1  21251  selberg4lem1  21254  selberg4  21255  pntrsumo1  21259  pntrlog2bndlem2  21272  pntrlog2bndlem3  21273  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  pntibndlem1  21283  pntibndlem2  21285  pntibndlem3  21286  pntlemb  21291  pntlemr  21296  pntlemf  21299  pntlem3  21303  pnt  21308  qabvle  21319  padicabv  21324  ostth1  21327  uhgrares  21343  umgrares  21359  usgrares  21389  nbgraop  21436  nbgraf1o0  21456  cusgra0v  21469  cusgra1v  21470  cusgraexilem2  21476  sizeusglecusg  21495  isuvtx  21497  2trllemH  21552  wlkntrllem3  21561  2wlklem1  21597  constr3trllem3  21639  constr3pthlem3  21644  vdgr0  21671  eupatrl  21690  eupares  21697  vdegp1ai  21706  vdegp1bi  21707  vsfval  22114  ipasslem7  22337  minvecolem2  22377  h2hcau  22482  h2hlm  22483  hlimadd  22695  hhsscms  22779  chocunii  22803  occllem  22805  leopnmid  23641  opsqrlem1  23643  hmopidmchi  23654  mdslj1i  23822  addltmulALT  23949  imadifxp  24038  xaddeq0  24119  xrge0npcan  24216  xrge0tsmsd  24223  xpinpreima2  24305  cnre2csqlem  24308  tpr2rico  24310  mndpluscn  24312  pnfneige0  24336  qqhghm  24372  qqhrhm  24373  qqhcn  24375  qqhucn  24376  esumsplit  24447  esumpr  24457  esumfsup  24460  sigaclcu2  24503  pwsiga  24513  prsiga  24514  measvuni  24568  elmbfmvol2  24617  mbfmcnt  24618  sxbrsigalem1  24635  sxbrsiga  24640  sibf0  24649  sitgclg  24656  isrrvv  24701  rrvadd  24710  rrvmulc  24711  dstrvprob  24729  coinflipspace  24738  coinfliprv  24740  ballotlemfmpn  24752  ballotlem1ri  24792  lgamcvg2  24839  gamcvg2lem  24843  indispcon  24921  conpcon  24922  iccllyscon  24937  cvmopnlem  24965  cvmliftlem15  24985  cvmlift2lem3  24992  circum  25111  fprodfac  25296  fallfac0  25344  bpoly4  26105  elhf2  26116  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  itg2addnclem  26256  ftc1anclem5  26284  dvreasin  26290  dvreacos  26291  areacirclem1  26292  areacirc  26297  bnd2lem  26500  prdsbnd  26502  cntotbnd  26505  cnpwstotbnd  26506  isdrngo2  26574  prter2  26730  isnacs3  26764  diophrw  26817  lzenom  26828  diophin  26831  pellexlem5  26896  pw2f1ocnv  27108  dnnumch2  27120  kelac2lem  27139  kelac2  27140  dfac21  27141  pwssplit1  27165  uvcvv1  27215  pwfi2f1o  27237  frlmpwfi  27239  lsslinds  27278  mpaaeu  27332  rngunsnply  27355  psgnunilem5  27394  matmulr  27444  mendbas  27469  mendplusgfval  27470  mendmulrfval  27472  mendsca  27474  mendvscafval  27475  subrgacs  27485  sdrgacs  27486  cntzsdrg  27487  idomodle  27489  phisum  27495  proot1ex  27497  deg1mhm  27503  ofsubid  27518  ofdivrec  27520  dvconstbi  27528  ioovolcl  27718  stoweidlem13  27738  stoweidlem26  27751  stoweidlem34  27759  stoweidlem42  27767  stoweidlem44  27769  stoweidlem48  27773  stoweidlem62  27787  stoweid  27788  stirlinglem7  27805  stirlinglem11  27809  reumodprminv  28227  cshwoor  28237  lswrd0  28261  swrdtrcfvl  28265  lswrdcshw  28266  cshwssizelem1a  28279  cshwssizensame  28289  cshwsexa  28291  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  frgra3v  28392  frgrancvvdeqlem9  28430  frgrancvvdgeq  28432  frg2wot1  28446  usgreghash2spotv  28455  eqlkr2  29898  tendoidcl  31566  cdlemk56  31768  dihpN  32134  mapdhval  32522  hlhillcs  32759
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator