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  5191  relcoi2  5330  isomin  5989  isoini  5990  dmtpos  6420  oaabs2  6817  mapsncnv  6989  boxcutc  7034  domunsncan  7137  pw2f1o  7142  unxpdom2  7246  sucxpdom  7247  ac6sfi  7280  xpfi  7307  imafi  7327  fifo  7365  ordtypelem4  7416  oismo  7435  wofib  7440  brwdom2  7467  canthwdom  7473  cantnflt  7553  cantnff  7555  cantnf0  7556  cantnfp1lem1  7560  cantnfp1lem3  7562  cantnflem1b  7568  cantnflem1d  7570  cantnflem1  7571  cnfcom  7583  cnfcom2lem  7584  ranksnb  7679  tskwe  7763  cardidm  7772  infxpenc  7825  fseqdom  7833  dfac8clem  7839  dfac12lem2  7950  infmap2  8024  isfin4-3  8121  fin23lem14  8139  fin23lem40  8157  isf34lem7  8185  isf34lem6  8186  fin1a2lem12  8217  hsmexlem4  8235  hsmexlem5  8236  ac5b  8284  alephexp1  8380  alephsuc3  8381  axpowndlem2  8399  fpwwe2lem8  8438  fpwwe2lem13  8443  canthwe  8452  canthp1lem2  8454  gchcda1  8457  pwfseqlem5  8464  wunco  8534  prlem934  8836  supsrlem  8912  msqge0  9474  ofnegsub  9923  ofsubge0  9924  xaddpnf1  10737  supxrmnf  10821  injresinjlem  11119  uzindi  11240  seqfeq4  11292  seqof  11300  bcval5  11529  hashdomi  11574  hash1snb  11601  brfi1uzind  11635  ccatlen  11664  s111  11682  wrdeqs1cat  11709  shftfib  11807  limsupcl  12187  limsupgf  12189  limsupval2  12194  isercolllem3  12380  ackbijnn  12527  supcvg  12555  ege2le3  12612  rpnnen2lem5  12738  ruclem11  12759  fsumdvds  12813  bitsinv2  12875  sadaddlem  12898  smupf  12910  smup0  12911  smu01lem  12917  isprm6  13029  hashdvds  13084  vdwlem13  13281  ramtlecl  13288  0ram  13308  prmlem0  13348  wunndx  13405  prdsval  13598  xpsbas  13719  xpsadd  13721  xpsmul  13722  xpssca  13723  xpsvsca  13724  xpsless  13725  xpsle  13726  mreexexlem2d  13790  mreacs  13803  acsfn  13804  idfu2nd  13994  idfucl  13998  fucsect  14089  setccatid  14159  setcepi  14163  catchomfval  14173  uncfval  14251  oduglb  14486  odumeet  14487  odulub  14488  odujoin  14489  isipodrs  14507  fpwipodrs  14510  isacs4lem  14514  isacs5lem  14515  submacs  14685  frmdup1  14729  mulgneg2  14837  subgacs  14895  nsgacs  14896  odf1o2  15127  frgpuplem  15324  cygctb  15421  gsum2d  15466  dprdsubg  15502  dmdprdsplit2lem  15523  dmdprdpr  15527  dprdpr  15528  dpjeq  15537  ablfac1eulem  15550  pgpfac1lem2  15553  pgpfaclem1  15559  unitgrp  15692  isirred  15724  lssacs  15963  lbsextlem2  16151  lbsextlem3  16152  psrlidm  16387  resspsradd  16399  resspsrmul  16400  resspsrvsca  16401  ltbwe  16453  coe1add  16577  coe1mul2lem1  16580  coe1tm  16585  xrsmcmn  16640  xrs1mnd  16652  xrs10  16653  gsumfsum  16682  zlpirlem3  16686  zlpir  16687  zcyg  16688  mulgrhm  16703  mulgrhm2  16704  zlmlmod  16720  zlmassa  16721  znbas  16740  znzrhfo  16744  zndvds  16746  frgpcyg  16770  indistopon  16981  mreclatdemo  17076  mnfnei  17200  resthauslem  17342  sshauslem  17351  discmp  17376  conima  17402  1stcfb  17422  hauseqlcld  17592  xkoptsub  17600  xkofvcn  17630  idqtop  17652  tgqtop  17658  kqdisj  17678  xpstopnlem1  17755  xpstopnlem2  17757  ufildom1  17872  alexsubb  17991  alexsubALTlem3  17994  ptcmplem2  17998  ptcmplem3  17999  tmdgsum  18039  ustneism  18167  ustuqtop1  18185  iducn  18227  prdsmet  18301  imasdsf1olem  18304  xpsxmet  18311  xpsdsval  18312  xpsmet  18313  prdsbl  18404  met1stc  18434  prdsxmslem2  18442  xpsxms  18447  xpsms  18448  dscmet  18484  nmoffn  18609  nmofval  18612  nmolb  18615  nmof  18617  cnbl0  18672  xrsmopn  18707  xrge0gsumle  18728  xrge0tsms  18729  negfcncf  18813  cnrehmeo  18842  lebnum  18853  xlebnum  18854  reparphti  18886  pcopt  18911  pcopt2  18912  pcorevcl  18914  pcorevlem  18915  pi1xfrval  18943  pi1xfrcnvlem  18945  pi1xfrcnv  18946  pi1cof  18948  pi1coval  18949  nmhmcn  18992  cphsubrglem  19004  csscld  19067  cmetcaulem  19105  cmpcmet  19134  ovolunlem1  19253  ovolicc2lem4  19276  ioorcl2  19324  uniioovol  19331  uniioombllem4  19338  uniioombllem5  19339  uniioombllem6  19340  dyadmbllem  19351  mbfsub  19414  itg1climres  19466  xrge0f  19483  itg2ge0  19487  itg2i1fseq2  19508  ibl0  19538  ellimc2  19624  limcflf  19628  dvreslem  19656  dvidlem  19662  dvid  19664  cpnres  19683  dvaddbr  19684  dvmulbr  19685  dvfre  19697  dvexp  19699  dvrec  19701  dvmptid  19703  dvmptc  19704  dvmptntr  19717  dvexp3  19722  dvlipcn  19738  dveq0  19744  dv11cn  19745  lhop2  19759  ftc1a  19781  evl1rhm  19809  evl1sca  19810  evl1var  19812  pf1mpf  19832  pf1ind  19835  tdeglem1  19841  tdeglem3  19842  tdeglem4  19843  tdeglem2  19844  mdegle0  19860  ply1remlem  19945  fta1glem2  19949  plypf1  19991  coe0  20034  dvply1  20061  elqaalem3  20098  aaliou2b  20118  aaliou3lem8  20122  aaliou3lem7  20126  taylfvallem  20134  taylf  20137  tayl0  20138  taylpfval  20141  taylply  20145  dvtaylp  20146  taylthlem1  20149  taylthlem2  20150  ulmdvlem1  20176  ulmdvlem2  20177  ulmdvlem3  20178  radcnvcl  20193  psercnlem2  20200  psercn  20202  pserdv  20205  abelthlem3  20209  abelth  20217  sincn  20220  coscn  20221  reefgim  20226  tangtx  20273  pige3  20285  cosordlem  20293  logcn  20398  dvlog  20402  advlog  20405  advlogexp  20406  logtayl  20411  logccv  20414  dvcxp1  20486  cxpcn3lem  20491  cxpcn3  20492  resqrcn  20493  sqrcn  20494  loglesqr  20502  isosctrlem2  20523  dquartlem1  20551  quart  20561  atancj  20610  efiatan  20612  atantan  20623  atanbndlem  20625  atansopn  20632  dvatan  20635  atantayl  20637  leibpilem2  20641  leibpi  20642  log2tlbnd  20645  rlimcnp2  20665  efrlim  20668  divsqrsumlem  20678  jensenlem1  20685  jensenlem2  20686  jensen  20687  amgmlem  20688  amgm  20689  emcllem4  20697  emcllem7  20700  wilthlem2  20712  wilthlem3  20713  basellem6  20728  chtrpcl  20818  ppiltx  20820  1sgm2ppw  20844  chtlepsi  20850  chpub  20864  logfacbnd3  20867  logfacrlim  20868  perfectlem2  20874  dchrelbas2  20881  dchrabs  20904  dchrhash  20915  bposlem7  20934  lgsdir2lem5  20971  lgsqrlem1  20985  lgseisenlem4  20996  lgsquad2lem1  21002  lgsquad3  21005  chpo1ub  21034  vmadivsumb  21037  rpvmasumlem  21041  dchrisumlem2  21044  dchrmusumlema  21047  dchrvmasumlem2  21052  dchrvmasumlema  21054  dchrvmasumiflem1  21055  dchrisum0flblem1  21062  dchrisum0lem1  21070  rplogsum  21081  mudivsum  21084  logdivsum  21087  mulog2sumlem2  21089  vmalogdivsum2  21092  2vmadivsumlem  21094  log2sumbnd  21098  selberglem2  21100  selbergb  21103  selberg2lem  21104  selberg2b  21106  selberg3lem1  21111  selberg4lem1  21114  selberg4  21115  pntrsumo1  21119  pntrlog2bndlem2  21132  pntrlog2bndlem3  21133  pntrlog2bndlem4  21134  pntrlog2bndlem5  21135  pntibndlem1  21143  pntibndlem2  21145  pntibndlem3  21146  pntlemb  21151  pntlemr  21156  pntlemf  21159  pntlem3  21163  pnt  21168  qabvle  21179  padicabv  21184  ostth1  21187  uhgrares  21203  umgrares  21219  usgrares  21249  nbgraop  21295  nbgraf1o0  21315  cusgra0v  21328  cusgra1v  21329  cusgraexilem2  21335  sizeusglecusg  21354  isuvtx  21356  wlkntrllem5  21410  constr2trl  21439  constr3trllem3  21480  constr3pthlem3  21485  vdgr0  21512  eupatrl  21531  eupares  21538  vdegp1ai  21547  vdegp1bi  21548  vsfval  21955  ipasslem7  22178  minvecolem2  22218  h2hcau  22323  h2hlm  22324  hlimadd  22536  hhsscms  22620  chocunii  22644  occllem  22646  leopnmid  23482  opsqrlem1  23484  hmopidmchi  23495  mdslj1i  23663  addltmulALT  23790  imadifxp  23874  xaddeq0  24023  xrge0npcan  24038  xrge0tsmsd  24045  xpinpreima2  24102  cnre2csqlem  24105  tpr2rico  24107  mndpluscn  24109  pnfneige0  24133  qqhghm  24164  qqhrhm  24165  qqhcn  24167  qqhucn  24168  esumsplit  24236  esumpr  24246  esumfsup  24249  sigaclcu2  24292  pwsiga  24302  prsiga  24303  measvuni  24355  elmbfmvol2  24404  mbfmcnt  24405  sxbrsigalem1  24422  sxbrsiga  24427  isrrvv  24473  rrvadd  24482  rrvmulc  24483  dstrvprob  24501  coinflipspace  24510  coinfliprv  24512  ballotlemfmpn  24524  ballotlem1ri  24564  lgamcvg2  24611  gamcvg2lem  24615  indispcon  24693  conpcon  24694  iccllyscon  24709  cvmopnlem  24737  cvmliftlem15  24757  cvmlift2lem3  24764  circum  24883  fprodfac  25068  fallfac0  25105  bpoly4  25812  elhf2  25823  ovoliunnfl  25946  voliunnfl  25948  volsupnfl  25949  itg2addnclem  25950  itg2addnc  25952  dvreasin  25973  dvreacos  25974  areacirclem2  25975  areacirclem3  25976  bnd2lem  26184  prdsbnd  26186  cntotbnd  26189  cnpwstotbnd  26190  isdrngo2  26258  prter2  26414  isnacs3  26448  diophrw  26501  lzenom  26512  diophin  26515  pellexlem5  26580  pw2f1ocnv  26792  dnnumch2  26804  kelac2lem  26824  kelac2  26825  dfac21  26826  pwssplit1  26850  uvcvv1  26900  pwfi2f1o  26922  frlmpwfi  26924  lsslinds  26963  mpaaeu  27017  rngunsnply  27040  psgnunilem5  27079  matmulr  27129  mendbas  27154  mendplusgfval  27155  mendmulrfval  27157  mendsca  27159  mendvscafval  27160  subrgacs  27170  sdrgacs  27171  cntzsdrg  27172  idomodle  27174  phisum  27180  proot1ex  27182  deg1mhm  27188  ofsubid  27203  ofdivrec  27205  dvconstbi  27213  ioovolcl  27403  stoweidlem13  27423  stoweidlem26  27436  stoweidlem34  27444  stoweidlem42  27452  stoweidlem44  27454  stoweidlem48  27458  stoweidlem62  27472  stoweid  27473  stirlinglem7  27490  stirlinglem11  27494  frgra3v  27748  frgrancvvdeqlem9  27786  frgrancvvdgeq  27788  eqlkr2  29266  tendoidcl  30934  cdlemk56  31136  dihpN  31502  mapdhval  31890  hlhillcs  32127
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator