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  5083  relcoi2  5216  isomin  5850  isoini  5851  dmtpos  6262  oaabs2  6659  mapsncnv  6830  boxcutc  6875  domunsncan  6978  pw2f1o  6983  unxpdom2  7087  sucxpdom  7088  ac6sfi  7117  xpfi  7144  imafi  7164  fifo  7201  ordtypelem4  7252  oismo  7271  wofib  7276  brwdom2  7303  canthwdom  7309  cantnflt  7389  cantnff  7391  cantnf0  7392  cantnfp1lem1  7396  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  cnfcom  7419  cnfcom2lem  7420  ranksnb  7515  tskwe  7599  cardidm  7608  infxpenc  7661  fseqdom  7669  dfac8clem  7675  dfac12lem2  7786  infmap2  7860  isfin4-3  7957  fin23lem14  7975  fin23lem40  7993  isf34lem7  8021  isf34lem6  8022  fin1a2lem12  8053  hsmexlem4  8071  hsmexlem5  8072  ac5b  8121  alephexp1  8217  alephsuc3  8218  axpowndlem2  8236  fpwwe2lem8  8275  fpwwe2lem13  8280  canthwe  8289  canthp1lem2  8291  gchcda1  8294  pwfseqlem5  8301  wunco  8371  prlem934  8673  supsrlem  8749  msqge0  9311  ofnegsub  9760  ofsubge0  9761  xaddpnf1  10569  supxrmnf  10652  uzindi  11059  seqfeq4  11111  seqof  11119  bcval5  11346  hashdomi  11378  ccatlen  11446  s111  11464  wrdeqs1cat  11491  shftfib  11583  limsupcl  11963  limsupgf  11965  limsupval2  11970  isercolllem3  12156  ackbijnn  12302  supcvg  12330  ege2le3  12387  rpnnen2lem5  12513  ruclem11  12534  fsumdvds  12588  bitsinv2  12650  sadaddlem  12673  smupf  12685  smup0  12686  smu01lem  12692  isprm6  12804  hashdvds  12859  vdwlem13  13056  ramtlecl  13063  0ram  13083  prmlem0  13123  wunndx  13180  prdsval  13371  xpsbas  13492  xpsadd  13494  xpsmul  13495  xpssca  13496  xpsvsca  13497  xpsless  13498  xpsle  13499  mreexexlem2d  13563  mreacs  13576  acsfn  13577  idfu2nd  13767  idfucl  13771  fucsect  13862  setccatid  13932  setcepi  13936  catchomfval  13946  uncfval  14024  oduglb  14259  odumeet  14260  odulub  14261  odujoin  14262  isipodrs  14280  fpwipodrs  14283  isacs4lem  14287  isacs5lem  14288  submacs  14458  frmdup1  14502  mulgneg2  14610  subgacs  14668  nsgacs  14669  odf1o2  14900  frgpuplem  15097  cygctb  15194  gsum2d  15239  dprdsubg  15275  dmdprdsplit2lem  15296  dmdprdpr  15300  dprdpr  15301  dpjeq  15310  ablfac1eulem  15323  pgpfac1lem2  15326  pgpfaclem1  15332  unitgrp  15465  isirred  15497  lssacs  15740  lbsextlem2  15928  lbsextlem3  15929  psrlidm  16164  resspsradd  16176  resspsrmul  16177  resspsrvsca  16178  ltbwe  16230  coe1add  16357  coe1mul2lem1  16360  coe1tm  16365  xrsmcmn  16413  xrs1mnd  16425  xrs10  16426  gsumfsum  16455  zlpirlem3  16459  zlpir  16460  zcyg  16461  mulgrhm  16476  mulgrhm2  16477  zlmlmod  16493  zlmassa  16494  znbas  16513  znzrhfo  16517  zndvds  16519  frgpcyg  16543  indistopon  16754  mreclatdemo  16849  mnfnei  16967  resthauslem  17107  sshauslem  17116  discmp  17141  conima  17167  1stcfb  17187  hauseqlcld  17356  xkoptsub  17364  xkofvcn  17394  idqtop  17413  tgqtop  17419  kqdisj  17439  xpstopnlem1  17516  xpstopnlem2  17518  ufildom1  17637  alexsubb  17756  alexsubALTlem3  17759  ptcmplem2  17763  ptcmplem3  17764  tmdgsum  17794  prdsmet  17950  imasdsf1olem  17953  xpsxmet  17960  xpsdsval  17961  xpsmet  17962  prdsbl  18053  met1stc  18083  prdsxmslem2  18091  xpsxms  18096  xpsms  18097  dscmet  18111  nmoffn  18236  nmofval  18239  nmolb  18242  nmof  18244  cnbl0  18299  xrsmopn  18334  xrge0gsumle  18354  xrge0tsms  18355  negfcncf  18438  cnrehmeo  18467  lebnum  18478  xlebnum  18479  reparphti  18511  pcopt  18536  pcopt2  18537  pcorevcl  18539  pcorevlem  18540  pi1xfrval  18568  pi1xfrcnvlem  18570  pi1xfrcnv  18571  pi1cof  18573  pi1coval  18574  nmhmcn  18617  cphsubrglem  18629  csscld  18692  cmetcaulem  18730  cmpcmet  18759  ovolunlem1  18872  ovolicc2lem4  18895  ioorcl2  18943  uniioovol  18950  uniioombllem5  18958  uniioombllem6  18959  dyadmbllem  18970  mbfsub  19033  itg1climres  19085  xrge0f  19102  itg2ge0  19106  itg2i1fseq2  19127  ibl0  19157  ellimc2  19243  limcflf  19247  dvreslem  19275  dvidlem  19281  dvid  19283  cpnres  19302  dvaddbr  19303  dvmulbr  19304  dvfre  19316  dvexp  19318  dvrec  19320  dvmptid  19322  dvmptc  19323  dvmptntr  19336  dvexp3  19341  dvlipcn  19357  dveq0  19363  dv11cn  19364  lhop2  19378  ftc1a  19400  evl1rhm  19428  evl1sca  19429  evl1var  19431  pf1mpf  19451  pf1ind  19454  tdeglem1  19460  tdeglem3  19461  tdeglem4  19462  tdeglem2  19463  mdegle0  19479  ply1remlem  19564  fta1glem2  19568  plypf1  19610  coe0  19653  dvply1  19680  elqaalem3  19717  aaliou2b  19737  aaliou3lem8  19741  aaliou3lem7  19745  taylfvallem  19753  taylf  19756  tayl0  19757  taylpfval  19760  taylply  19764  dvtaylp  19765  taylthlem1  19768  taylthlem2  19769  ulmdvlem1  19793  ulmdvlem2  19794  ulmdvlem3  19795  radcnvcl  19809  psercnlem2  19816  psercn  19818  pserdv  19821  abelthlem3  19825  abelth  19833  sincn  19836  coscn  19837  reefgim  19842  tangtx  19889  pige3  19901  cosordlem  19909  logcn  20010  dvlog  20014  advlog  20017  advlogexp  20018  logtayl  20023  logccv  20026  dvcxp1  20098  cxpcn3lem  20103  cxpcn3  20104  resqrcn  20105  sqrcn  20106  loglesqr  20114  isosctrlem2  20135  dquartlem1  20163  quart  20173  atancj  20222  efiatan  20224  atansopn  20244  dvatan  20247  atantayl  20249  leibpilem2  20253  leibpi  20254  log2tlbnd  20257  rlimcnp2  20277  efrlim  20280  divsqrsumlem  20290  jensenlem1  20297  jensenlem2  20298  jensen  20299  amgmlem  20300  amgm  20301  emcllem4  20308  emcllem7  20311  wilthlem2  20323  wilthlem3  20324  basellem6  20339  chtrpcl  20429  ppiltx  20431  1sgm2ppw  20455  chtlepsi  20461  chpub  20475  logfacbnd3  20478  logfacrlim  20479  perfectlem2  20485  dchrelbas2  20492  dchrabs  20515  dchrhash  20526  bposlem7  20545  lgsdir2lem5  20582  lgsqrlem1  20596  lgseisenlem4  20607  lgsquad2lem1  20613  lgsquad3  20616  chpo1ub  20645  vmadivsumb  20648  rpvmasumlem  20652  dchrisumlem2  20655  dchrmusumlema  20658  dchrvmasumlem2  20663  dchrvmasumlema  20665  dchrvmasumiflem1  20666  dchrisum0flblem1  20673  dchrisum0lem1  20681  rplogsum  20692  mudivsum  20695  logdivsum  20698  mulog2sumlem2  20700  vmalogdivsum2  20703  2vmadivsumlem  20705  log2sumbnd  20709  selberglem2  20711  selbergb  20714  selberg2lem  20715  selberg2b  20717  selberg3lem1  20722  selberg4lem1  20725  selberg4  20726  pntrsumo1  20730  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntibndlem1  20754  pntibndlem2  20756  pntibndlem3  20757  pntlemb  20762  pntlemr  20767  pntlemf  20770  pntlem3  20774  pnt  20779  qabvle  20790  padicabv  20795  ostth1  20798  vsfval  21207  ipasslem7  21430  minvecolem2  21470  h2hcau  21575  h2hlm  21576  hlimadd  21788  hhsscms  21872  chocunii  21896  occllem  21898  leopnmid  22734  opsqrlem1  22736  hmopidmchi  22747  mdslj1i  22915  addltmulALT  23042  ballotlem1ri  23109  cnre2csqlem  23309  tpr2rico  23311  mndpluscn  23314  xrge0npcan  23348  pnfneige0  23389  xrge0tsmsd  23397  esumsplit  23446  sigaclcu2  23496  pwsiga  23506  prsiga  23507  measvuni  23557  elmbfmvol2  23587  dya2iocct  23596  isrrvv  23661  rrvmulc  23670  coinflipspace  23696  coinfliprv  23698  indispcon  23780  conpcon  23781  iccllyscon  23796  cvmopnlem  23824  cvmliftlem15  23844  cvmlift2lem3  23851  umgrares  23891  vdgr0  23907  eupares  23914  vdegp1ai  23923  vdegp1bi  23924  circum  24022  bpoly4  24866  elhf2  24877  ovoliunnfl  25001  itg2addnclem  25003  itg2addnc  25005  dvreasin  25026  dvreacos  25027  areacirclem2  25028  areacirclem3  25029  splint  25151  cnvref2  25169  imfstnrelc  25184  prjcp1  25187  prjcp2  25188  cbcpcp  25265  domrancur1c  25305  ubos  25359  fprodser  25423  supnuf  25732  claddrv  25750  sigadd  25752  valvze  25757  addassv  25759  rnegvex2  25764  issubrv  25775  subclrvd  25777  clsmulcv  25785  clsmulrv  25786  fnmulcv  25787  icccon4  25805  aidm2  25853  dualalg  25885  idfisf  25944  idsubfun  25961  isinob  25965  isntr  25976  islimcat  25979  isgraphmrph  26026  cmpidmor3  26073  setiscat  26082  isconc2  26110  isconc3  26111  pgapspf  26155  pgapspf2  26156  linevala2  26181  lineval3a  26186  sgplpte22  26241  nds  26253  isray2  26256  pdiveql  26271  aishp  26275  bnd2lem  26618  prdsbnd  26620  cntotbnd  26623  cnpwstotbnd  26624  isdrngo2  26692  prter2  26852  isnacs3  26888  diophrw  26941  lzenom  26952  diophin  26955  pellexlem5  27021  pw2f1ocnv  27233  dnnumch2  27245  kelac2lem  27265  kelac2  27266  dfac21  27267  pwssplit1  27291  uvcvv1  27341  pwfi2f1o  27363  frlmpwfi  27365  lsslinds  27404  mpaaeu  27458  rngunsnply  27481  psgnunilem5  27520  matmulr  27570  mendbas  27595  mendplusgfval  27596  mendmulrfval  27598  mendsca  27600  mendvscafval  27601  subrgacs  27611  sdrgacs  27612  cntzsdrg  27613  idomodle  27615  phisum  27621  proot1ex  27623  deg1mhm  27629  ofsubid  27644  ofdivrec  27646  dvconstbi  27654  stoweidlem13  27865  stoweidlem62  27914  aibnbna  27977  injresinjlem  28214  usgrares  28249  nbgraop  28274  cusgra0v  28295  cusgra1v  28296  isuvtx  28301  wlkntrllem5  28349  eupatrl  28385  constr3trllem3  28398  constr3pthlem3  28403  frgra3v  28426  eqlkr2  29912  tendoidcl  31580  cdlemk56  31782  dihpN  32148  mapdhval  32536  hlhillcs  32773
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator