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

Theorem mp1i 11
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 10 1  |-  ( ch 
->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  poirr2  5067  relcoi2  5200  isomin  5834  isoini  5835  dmtpos  6246  oaabs2  6643  mapsncnv  6814  boxcutc  6859  domunsncan  6962  pw2f1o  6967  unxpdom2  7071  sucxpdom  7072  ac6sfi  7101  xpfi  7128  imafi  7148  fifo  7185  ordtypelem4  7236  oismo  7255  wofib  7260  brwdom2  7287  canthwdom  7293  cantnflt  7373  cantnff  7375  cantnf0  7376  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cnfcom  7403  cnfcom2lem  7404  ranksnb  7499  tskwe  7583  cardidm  7592  infxpenc  7645  fseqdom  7653  dfac8clem  7659  dfac12lem2  7770  infmap2  7844  isfin4-3  7941  fin23lem14  7959  fin23lem40  7977  isf34lem7  8005  isf34lem6  8006  fin1a2lem12  8037  hsmexlem4  8055  hsmexlem5  8056  ac5b  8105  alephexp1  8201  alephsuc3  8202  axpowndlem2  8220  fpwwe2lem8  8259  fpwwe2lem13  8264  canthwe  8273  canthp1lem2  8275  gchcda1  8278  pwfseqlem5  8285  wunco  8355  prlem934  8657  supsrlem  8733  msqge0  9295  ofnegsub  9744  ofsubge0  9745  xaddpnf1  10553  supxrmnf  10636  uzindi  11043  seqfeq4  11095  seqof  11103  bcval5  11330  hashdomi  11362  ccatlen  11430  s111  11448  wrdeqs1cat  11475  shftfib  11567  limsupcl  11947  limsupgf  11949  limsupval2  11954  isercolllem3  12140  ackbijnn  12286  supcvg  12314  ege2le3  12371  rpnnen2lem5  12497  ruclem11  12518  fsumdvds  12572  bitsinv2  12634  sadaddlem  12657  smupf  12669  smup0  12670  smu01lem  12676  isprm6  12788  hashdvds  12843  vdwlem13  13040  ramtlecl  13047  0ram  13067  prmlem0  13107  wunndx  13164  prdsval  13355  xpsbas  13476  xpsadd  13478  xpsmul  13479  xpssca  13480  xpsvsca  13481  xpsless  13482  xpsle  13483  mreexexlem2d  13547  mreacs  13560  acsfn  13561  idfu2nd  13751  idfucl  13755  fucsect  13846  setccatid  13916  setcepi  13920  catchomfval  13930  uncfval  14008  oduglb  14243  odumeet  14244  odulub  14245  odujoin  14246  isipodrs  14264  fpwipodrs  14267  isacs4lem  14271  isacs5lem  14272  submacs  14442  frmdup1  14486  mulgneg2  14594  subgacs  14652  nsgacs  14653  odf1o2  14884  frgpuplem  15081  cygctb  15178  gsum2d  15223  dprdsubg  15259  dmdprdsplit2lem  15280  dmdprdpr  15284  dprdpr  15285  dpjeq  15294  ablfac1eulem  15307  pgpfac1lem2  15310  pgpfaclem1  15316  unitgrp  15449  isirred  15481  lssacs  15724  lbsextlem2  15912  lbsextlem3  15913  psrlidm  16148  resspsradd  16160  resspsrmul  16161  resspsrvsca  16162  ltbwe  16214  coe1add  16341  coe1mul2lem1  16344  coe1tm  16349  xrsmcmn  16397  xrs1mnd  16409  xrs10  16410  gsumfsum  16439  zlpirlem3  16443  zlpir  16444  zcyg  16445  mulgrhm  16460  mulgrhm2  16461  zlmlmod  16477  zlmassa  16478  znbas  16497  znzrhfo  16501  zndvds  16503  frgpcyg  16527  indistopon  16738  mreclatdemo  16833  mnfnei  16951  resthauslem  17091  sshauslem  17100  discmp  17125  conima  17151  1stcfb  17171  hauseqlcld  17340  xkoptsub  17348  xkofvcn  17378  idqtop  17397  tgqtop  17403  kqdisj  17423  xpstopnlem1  17500  xpstopnlem2  17502  ufildom1  17621  alexsubb  17740  alexsubALTlem3  17743  ptcmplem2  17747  ptcmplem3  17748  tmdgsum  17778  prdsmet  17934  imasdsf1olem  17937  xpsxmet  17944  xpsdsval  17945  xpsmet  17946  prdsbl  18037  met1stc  18067  prdsxmslem2  18075  xpsxms  18080  xpsms  18081  dscmet  18095  nmoffn  18220  nmofval  18223  nmolb  18226  nmof  18228  cnbl0  18283  xrsmopn  18318  xrge0gsumle  18338  xrge0tsms  18339  negfcncf  18422  cnrehmeo  18451  lebnum  18462  xlebnum  18463  reparphti  18495  pcopt  18520  pcopt2  18521  pcorevcl  18523  pcorevlem  18524  pi1xfrval  18552  pi1xfrcnvlem  18554  pi1xfrcnv  18555  pi1cof  18557  pi1coval  18558  nmhmcn  18601  cphsubrglem  18613  csscld  18676  cmetcaulem  18714  cmpcmet  18743  ovolunlem1  18856  ovolicc2lem4  18879  ioorcl2  18927  uniioovol  18934  uniioombllem5  18942  uniioombllem6  18943  dyadmbllem  18954  mbfsub  19017  itg1climres  19069  xrge0f  19086  itg2ge0  19090  itg2i1fseq2  19111  ibl0  19141  ellimc2  19227  limcflf  19231  dvreslem  19259  dvidlem  19265  dvid  19267  cpnres  19286  dvaddbr  19287  dvmulbr  19288  dvfre  19300  dvexp  19302  dvrec  19304  dvmptid  19306  dvmptc  19307  dvmptntr  19320  dvexp3  19325  dvlipcn  19341  dveq0  19347  dv11cn  19348  lhop2  19362  ftc1a  19384  evl1rhm  19412  evl1sca  19413  evl1var  19415  pf1mpf  19435  pf1ind  19438  tdeglem1  19444  tdeglem3  19445  tdeglem4  19446  tdeglem2  19447  mdegle0  19463  ply1remlem  19548  fta1glem2  19552  plypf1  19594  coe0  19637  dvply1  19664  elqaalem3  19701  aaliou2b  19721  aaliou3lem8  19725  aaliou3lem7  19729  taylfvallem  19737  taylf  19740  tayl0  19741  taylpfval  19744  taylply  19748  dvtaylp  19749  taylthlem1  19752  taylthlem2  19753  ulmdvlem1  19777  ulmdvlem2  19778  ulmdvlem3  19779  radcnvcl  19793  psercnlem2  19800  psercn  19802  pserdv  19805  abelthlem3  19809  abelth  19817  sincn  19820  coscn  19821  reefgim  19826  tangtx  19873  pige3  19885  cosordlem  19893  logcn  19994  dvlog  19998  advlog  20001  advlogexp  20002  logtayl  20007  logccv  20010  dvcxp1  20082  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  sqrcn  20090  loglesqr  20098  isosctrlem2  20119  dquartlem1  20147  quart  20157  atancj  20206  efiatan  20208  atansopn  20228  dvatan  20231  atantayl  20233  leibpilem2  20237  leibpi  20238  log2tlbnd  20241  rlimcnp2  20261  efrlim  20264  divsqrsumlem  20274  jensenlem1  20281  jensenlem2  20282  jensen  20283  amgmlem  20284  amgm  20285  emcllem4  20292  emcllem7  20295  wilthlem2  20307  wilthlem3  20308  basellem6  20323  chtrpcl  20413  ppiltx  20415  1sgm2ppw  20439  chtlepsi  20445  chpub  20459  logfacbnd3  20462  logfacrlim  20463  perfectlem2  20469  dchrelbas2  20476  dchrabs  20499  dchrhash  20510  bposlem7  20529  lgsdir2lem5  20566  lgsqrlem1  20580  lgseisenlem4  20591  lgsquad2lem1  20597  lgsquad3  20600  chpo1ub  20629  vmadivsumb  20632  rpvmasumlem  20636  dchrisumlem2  20639  dchrmusumlema  20642  dchrvmasumlem2  20647  dchrvmasumlema  20649  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0lem1  20665  rplogsum  20676  mudivsum  20679  logdivsum  20682  mulog2sumlem2  20684  vmalogdivsum2  20687  2vmadivsumlem  20689  log2sumbnd  20693  selberglem2  20695  selbergb  20698  selberg2lem  20699  selberg2b  20701  selberg3lem1  20706  selberg4lem1  20709  selberg4  20710  pntrsumo1  20714  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntibndlem1  20738  pntibndlem2  20740  pntibndlem3  20741  pntlemb  20746  pntlemr  20751  pntlemf  20754  pntlem3  20758  pnt  20763  qabvle  20774  padicabv  20779  ostth1  20782  vsfval  21191  ipasslem7  21414  minvecolem2  21454  h2hcau  21559  h2hlm  21560  hlimadd  21772  hhsscms  21856  chocunii  21880  occllem  21882  leopnmid  22718  opsqrlem1  22720  hmopidmchi  22731  mdslj1i  22899  addltmulALT  23026  ballotlem1ri  23093  cnre2csqlem  23294  tpr2rico  23296  mndpluscn  23299  xrge0npcan  23333  pnfneige0  23374  xrge0tsmsd  23382  esumsplit  23431  sigaclcu2  23481  pwsiga  23491  prsiga  23492  measvuni  23542  elmbfmvol2  23572  dya2iocct  23581  isrrvv  23646  rrvmulc  23655  coinflipspace  23681  coinfliprv  23683  indispcon  23765  conpcon  23766  iccllyscon  23781  cvmopnlem  23809  cvmliftlem15  23829  cvmlift2lem3  23836  umgrares  23876  vdgr0  23892  eupares  23899  vdegp1ai  23908  vdegp1bi  23909  circum  24007  bpoly4  24794  elhf2  24805  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem3  24926  splint  25048  cnvref2  25066  imfstnrelc  25081  prjcp1  25084  prjcp2  25085  cbcpcp  25162  domrancur1c  25202  ubos  25256  fprodser  25320  supnuf  25629  claddrv  25647  sigadd  25649  valvze  25654  addassv  25656  rnegvex2  25661  issubrv  25672  subclrvd  25674  clsmulcv  25682  clsmulrv  25683  fnmulcv  25684  icccon4  25702  aidm2  25750  dualalg  25782  idfisf  25841  idsubfun  25858  isinob  25862  isntr  25873  islimcat  25876  isgraphmrph  25923  cmpidmor3  25970  setiscat  25979  isconc2  26007  isconc3  26008  pgapspf  26052  pgapspf2  26053  linevala2  26078  lineval3a  26083  sgplpte22  26138  nds  26150  isray2  26153  pdiveql  26168  aishp  26172  bnd2lem  26515  prdsbnd  26517  cntotbnd  26520  cnpwstotbnd  26521  isdrngo2  26589  prter2  26749  isnacs3  26785  diophrw  26838  lzenom  26849  diophin  26852  pellexlem5  26918  pw2f1ocnv  27130  dnnumch2  27142  kelac2lem  27162  kelac2  27163  dfac21  27164  pwssplit1  27188  uvcvv1  27238  pwfi2f1o  27260  frlmpwfi  27262  lsslinds  27301  mpaaeu  27355  rngunsnply  27378  psgnunilem5  27417  matmulr  27467  mendbas  27492  mendplusgfval  27493  mendmulrfval  27495  mendsca  27497  mendvscafval  27498  subrgacs  27508  sdrgacs  27509  cntzsdrg  27510  idomodle  27512  phisum  27518  proot1ex  27520  deg1mhm  27526  ofsubid  27541  ofdivrec  27543  dvconstbi  27551  stoweidlem13  27762  stoweidlem62  27811  aibnbna  27874  usgrares  28115  nbgraop  28140  cusgra0v  28156  cusgra1v  28157  isuvtx  28160  frgra3v  28180  eqlkr2  29290  tendoidcl  30958  cdlemk56  31160  dihpN  31526  mapdhval  31914  hlhillcs  32151
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator