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  5069  relcoi2  5202  isomin  5836  isoini  5837  dmtpos  6248  oaabs2  6645  mapsncnv  6816  boxcutc  6861  domunsncan  6964  pw2f1o  6969  unxpdom2  7073  sucxpdom  7074  ac6sfi  7103  xpfi  7130  imafi  7150  fifo  7187  ordtypelem4  7238  oismo  7257  wofib  7262  brwdom2  7289  canthwdom  7295  cantnflt  7375  cantnff  7377  cantnf0  7378  cantnfp1lem1  7382  cantnfp1lem3  7384  cantnflem1b  7390  cantnflem1d  7392  cantnflem1  7393  cnfcom  7405  cnfcom2lem  7406  ranksnb  7501  tskwe  7585  cardidm  7594  infxpenc  7647  fseqdom  7655  dfac8clem  7661  dfac12lem2  7772  infmap2  7846  isfin4-3  7943  fin23lem14  7961  fin23lem40  7979  isf34lem7  8007  isf34lem6  8008  fin1a2lem12  8039  hsmexlem4  8057  hsmexlem5  8058  ac5b  8107  alephexp1  8203  alephsuc3  8204  axpowndlem2  8222  fpwwe2lem8  8261  fpwwe2lem13  8266  canthwe  8275  canthp1lem2  8277  gchcda1  8280  pwfseqlem5  8287  wunco  8357  prlem934  8659  supsrlem  8735  msqge0  9297  ofnegsub  9746  ofsubge0  9747  xaddpnf1  10555  supxrmnf  10638  uzindi  11045  seqfeq4  11097  seqof  11105  bcval5  11332  hashdomi  11364  ccatlen  11432  s111  11450  wrdeqs1cat  11477  shftfib  11569  limsupcl  11949  limsupgf  11951  limsupval2  11956  isercolllem3  12142  ackbijnn  12288  supcvg  12316  ege2le3  12373  rpnnen2lem5  12499  ruclem11  12520  fsumdvds  12574  bitsinv2  12636  sadaddlem  12659  smupf  12671  smup0  12672  smu01lem  12678  isprm6  12790  hashdvds  12845  vdwlem13  13042  ramtlecl  13049  0ram  13069  prmlem0  13109  wunndx  13166  prdsval  13357  xpsbas  13478  xpsadd  13480  xpsmul  13481  xpssca  13482  xpsvsca  13483  xpsless  13484  xpsle  13485  mreexexlem2d  13549  mreacs  13562  acsfn  13563  idfu2nd  13753  idfucl  13757  fucsect  13848  setccatid  13918  setcepi  13922  catchomfval  13932  uncfval  14010  oduglb  14245  odumeet  14246  odulub  14247  odujoin  14248  isipodrs  14266  fpwipodrs  14269  isacs4lem  14273  isacs5lem  14274  submacs  14444  frmdup1  14488  mulgneg2  14596  subgacs  14654  nsgacs  14655  odf1o2  14886  frgpuplem  15083  cygctb  15180  gsum2d  15225  dprdsubg  15261  dmdprdsplit2lem  15282  dmdprdpr  15286  dprdpr  15287  dpjeq  15296  ablfac1eulem  15309  pgpfac1lem2  15312  pgpfaclem1  15318  unitgrp  15451  isirred  15483  lssacs  15726  lbsextlem2  15914  lbsextlem3  15915  psrlidm  16150  resspsradd  16162  resspsrmul  16163  resspsrvsca  16164  ltbwe  16216  coe1add  16343  coe1mul2lem1  16346  coe1tm  16351  xrsmcmn  16399  xrs1mnd  16411  xrs10  16412  gsumfsum  16441  zlpirlem3  16445  zlpir  16446  zcyg  16447  mulgrhm  16462  mulgrhm2  16463  zlmlmod  16479  zlmassa  16480  znbas  16499  znzrhfo  16503  zndvds  16505  frgpcyg  16529  indistopon  16740  mreclatdemo  16835  mnfnei  16953  resthauslem  17093  sshauslem  17102  discmp  17127  conima  17153  1stcfb  17173  hauseqlcld  17342  xkoptsub  17350  xkofvcn  17380  idqtop  17399  tgqtop  17405  kqdisj  17425  xpstopnlem1  17502  xpstopnlem2  17504  ufildom1  17623  alexsubb  17742  alexsubALTlem3  17745  ptcmplem2  17749  ptcmplem3  17750  tmdgsum  17780  prdsmet  17936  imasdsf1olem  17939  xpsxmet  17946  xpsdsval  17947  xpsmet  17948  prdsbl  18039  met1stc  18069  prdsxmslem2  18077  xpsxms  18082  xpsms  18083  dscmet  18097  nmoffn  18222  nmofval  18225  nmolb  18228  nmof  18230  cnbl0  18285  xrsmopn  18320  xrge0gsumle  18340  xrge0tsms  18341  negfcncf  18424  cnrehmeo  18453  lebnum  18464  xlebnum  18465  reparphti  18497  pcopt  18522  pcopt2  18523  pcorevcl  18525  pcorevlem  18526  pi1xfrval  18554  pi1xfrcnvlem  18556  pi1xfrcnv  18557  pi1cof  18559  pi1coval  18560  nmhmcn  18603  cphsubrglem  18615  csscld  18678  cmetcaulem  18716  cmpcmet  18745  ovolunlem1  18858  ovolicc2lem4  18881  ioorcl2  18929  uniioovol  18936  uniioombllem5  18944  uniioombllem6  18945  dyadmbllem  18956  mbfsub  19019  itg1climres  19071  xrge0f  19088  itg2ge0  19092  itg2i1fseq2  19113  ibl0  19143  ellimc2  19229  limcflf  19233  dvreslem  19261  dvidlem  19267  dvid  19269  cpnres  19288  dvaddbr  19289  dvmulbr  19290  dvfre  19302  dvexp  19304  dvrec  19306  dvmptid  19308  dvmptc  19309  dvmptntr  19322  dvexp3  19327  dvlipcn  19343  dveq0  19349  dv11cn  19350  lhop2  19364  ftc1a  19386  evl1rhm  19414  evl1sca  19415  evl1var  19417  pf1mpf  19437  pf1ind  19440  tdeglem1  19446  tdeglem3  19447  tdeglem4  19448  tdeglem2  19449  mdegle0  19465  ply1remlem  19550  fta1glem2  19554  plypf1  19596  coe0  19639  dvply1  19666  elqaalem3  19703  aaliou2b  19723  aaliou3lem8  19727  aaliou3lem7  19731  taylfvallem  19739  taylf  19742  tayl0  19743  taylpfval  19746  taylply  19750  dvtaylp  19751  taylthlem1  19754  taylthlem2  19755  ulmdvlem1  19779  ulmdvlem2  19780  ulmdvlem3  19781  radcnvcl  19795  psercnlem2  19802  psercn  19804  pserdv  19807  abelthlem3  19811  abelth  19819  sincn  19822  coscn  19823  reefgim  19828  tangtx  19875  pige3  19887  cosordlem  19895  logcn  19996  dvlog  20000  advlog  20003  advlogexp  20004  logtayl  20009  logccv  20012  dvcxp1  20084  cxpcn3lem  20089  cxpcn3  20090  resqrcn  20091  sqrcn  20092  loglesqr  20100  isosctrlem2  20121  dquartlem1  20149  quart  20159  atancj  20208  efiatan  20210  atansopn  20230  dvatan  20233  atantayl  20235  leibpilem2  20239  leibpi  20240  log2tlbnd  20243  rlimcnp2  20263  efrlim  20266  divsqrsumlem  20276  jensenlem1  20283  jensenlem2  20284  jensen  20285  amgmlem  20286  amgm  20287  emcllem4  20294  emcllem7  20297  wilthlem2  20309  wilthlem3  20310  basellem6  20325  chtrpcl  20415  ppiltx  20417  1sgm2ppw  20441  chtlepsi  20447  chpub  20461  logfacbnd3  20464  logfacrlim  20465  perfectlem2  20471  dchrelbas2  20478  dchrabs  20501  dchrhash  20512  bposlem7  20531  lgsdir2lem5  20568  lgsqrlem1  20582  lgseisenlem4  20593  lgsquad2lem1  20599  lgsquad3  20602  chpo1ub  20631  vmadivsumb  20634  rpvmasumlem  20638  dchrisumlem2  20641  dchrmusumlema  20644  dchrvmasumlem2  20649  dchrvmasumlema  20651  dchrvmasumiflem1  20652  dchrisum0flblem1  20659  dchrisum0lem1  20667  rplogsum  20678  mudivsum  20681  logdivsum  20684  mulog2sumlem2  20686  vmalogdivsum2  20689  2vmadivsumlem  20691  log2sumbnd  20695  selberglem2  20697  selbergb  20700  selberg2lem  20701  selberg2b  20703  selberg3lem1  20708  selberg4lem1  20711  selberg4  20712  pntrsumo1  20716  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntibndlem1  20740  pntibndlem2  20742  pntibndlem3  20743  pntlemb  20748  pntlemr  20753  pntlemf  20756  pntlem3  20760  pnt  20765  qabvle  20776  padicabv  20781  ostth1  20784  vsfval  21193  ipasslem7  21416  minvecolem2  21456  h2hcau  21561  h2hlm  21562  hlimadd  21774  hhsscms  21858  chocunii  21882  occllem  21884  leopnmid  22720  opsqrlem1  22722  hmopidmchi  22733  mdslj1i  22901  addltmulALT  23028  ballotlem1ri  23095  cnre2csqlem  23296  tpr2rico  23298  mndpluscn  23301  xrge0npcan  23335  pnfneige0  23376  xrge0tsmsd  23384  esumsplit  23433  sigaclcu2  23483  pwsiga  23493  prsiga  23494  measvuni  23544  elmbfmvol2  23574  dya2iocct  23583  isrrvv  23648  rrvmulc  23657  coinflipspace  23683  coinfliprv  23685  indispcon  23767  conpcon  23768  iccllyscon  23783  cvmopnlem  23811  cvmliftlem15  23831  cvmlift2lem3  23838  umgrares  23878  vdgr0  23894  eupares  23901  vdegp1ai  23910  vdegp1bi  23911  circum  24009  bpoly4  24796  elhf2  24807  dvreasin  24925  dvreacos  24926  itg2addnclem  24933  itg2addnc  24935  areacirclem2  24936  areacirclem3  24937  splint  25059  cnvref2  25077  imfstnrelc  25092  prjcp1  25095  prjcp2  25096  cbcpcp  25173  domrancur1c  25213  ubos  25267  fprodser  25331  supnuf  25640  claddrv  25658  sigadd  25660  valvze  25665  addassv  25667  rnegvex2  25672  issubrv  25683  subclrvd  25685  clsmulcv  25693  clsmulrv  25694  fnmulcv  25695  icccon4  25713  aidm2  25761  dualalg  25793  idfisf  25852  idsubfun  25869  isinob  25873  isntr  25884  islimcat  25887  isgraphmrph  25934  cmpidmor3  25981  setiscat  25990  isconc2  26018  isconc3  26019  pgapspf  26063  pgapspf2  26064  linevala2  26089  lineval3a  26094  sgplpte22  26149  nds  26161  isray2  26164  pdiveql  26179  aishp  26183  bnd2lem  26526  prdsbnd  26528  cntotbnd  26531  cnpwstotbnd  26532  isdrngo2  26600  prter2  26760  isnacs3  26796  diophrw  26849  lzenom  26860  diophin  26863  pellexlem5  26929  pw2f1ocnv  27141  dnnumch2  27153  kelac2lem  27173  kelac2  27174  dfac21  27175  pwssplit1  27199  uvcvv1  27249  pwfi2f1o  27271  frlmpwfi  27273  lsslinds  27312  mpaaeu  27366  rngunsnply  27389  psgnunilem5  27428  matmulr  27478  mendbas  27503  mendplusgfval  27504  mendmulrfval  27506  mendsca  27508  mendvscafval  27509  subrgacs  27519  sdrgacs  27520  cntzsdrg  27521  idomodle  27523  phisum  27529  proot1ex  27531  deg1mhm  27537  ofsubid  27552  ofdivrec  27554  dvconstbi  27562  stoweidlem13  27773  stoweidlem62  27822  aibnbna  27885  usgrares  28126  nbgraop  28151  cusgra0v  28167  cusgra1v  28168  isuvtx  28171  frgra3v  28191  eqlkr2  29363  tendoidcl  31031  cdlemk56  31233  dihpN  31599  mapdhval  31987  hlhillcs  32224
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator