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  5250  relcoi2  5389  isomin  6049  isoini  6050  dmtpos  6483  oaabs2  6880  mapsncnv  7052  boxcutc  7097  domunsncan  7200  pw2f1o  7205  unxpdom2  7309  sucxpdom  7310  ac6sfi  7343  xpfi  7370  imafi  7391  fifo  7429  ordtypelem4  7480  oismo  7499  wofib  7504  brwdom2  7531  canthwdom  7537  cantnflt  7617  cantnff  7619  cantnf0  7620  cantnfp1lem1  7624  cantnfp1lem3  7626  cantnflem1b  7632  cantnflem1d  7634  cantnflem1  7635  cnfcom  7647  cnfcom2lem  7648  ranksnb  7743  tskwe  7827  cardidm  7836  infxpenc  7889  fseqdom  7897  dfac8clem  7903  dfac12lem2  8014  infmap2  8088  isfin4-3  8185  fin23lem14  8203  fin23lem40  8221  isf34lem7  8249  isf34lem6  8250  fin1a2lem12  8281  hsmexlem4  8299  hsmexlem5  8300  ac5b  8348  alephexp1  8444  alephsuc3  8445  axpowndlem2  8463  fpwwe2lem8  8502  fpwwe2lem13  8507  canthwe  8516  canthp1lem2  8518  gchcda1  8521  pwfseqlem5  8528  wunco  8598  prlem934  8900  supsrlem  8976  msqge0  9539  ofnegsub  9988  ofsubge0  9989  xaddpnf1  10802  supxrmnf  10886  injresinjlem  11189  uzindi  11310  seqfeq4  11362  seqof  11370  bcval5  11599  hashdomi  11644  hash1snb  11671  brfi1uzind  11705  ccatlen  11734  s111  11752  wrdeqs1cat  11779  shftfib  11877  limsupcl  12257  limsupgf  12259  limsupval2  12264  isercolllem3  12450  ackbijnn  12597  supcvg  12625  ege2le3  12682  rpnnen2lem5  12808  ruclem11  12829  fsumdvds  12883  bitsinv2  12945  sadaddlem  12968  smupf  12980  smup0  12981  smu01lem  12987  isprm6  13099  hashdvds  13154  vdwlem13  13351  ramtlecl  13358  0ram  13378  prmlem0  13418  wunndx  13475  prdsval  13668  xpsbas  13789  xpsadd  13791  xpsmul  13792  xpssca  13793  xpsvsca  13794  xpsless  13795  xpsle  13796  mreexexlem2d  13860  mreacs  13873  acsfn  13874  idfu2nd  14064  idfucl  14068  fucsect  14159  setccatid  14229  setcepi  14233  catchomfval  14243  uncfval  14321  oduglb  14556  odumeet  14557  odulub  14558  odujoin  14559  isipodrs  14577  fpwipodrs  14580  isacs4lem  14584  isacs5lem  14585  submacs  14755  frmdup1  14799  mulgneg2  14907  subgacs  14965  nsgacs  14966  odf1o2  15197  frgpuplem  15394  cygctb  15491  gsum2d  15536  dprdsubg  15572  dmdprdsplit2lem  15593  dmdprdpr  15597  dprdpr  15598  dpjeq  15607  ablfac1eulem  15620  pgpfac1lem2  15623  pgpfaclem1  15629  unitgrp  15762  isirred  15794  lssacs  16033  lbsextlem2  16221  lbsextlem3  16222  psrlidm  16457  resspsradd  16469  resspsrmul  16470  resspsrvsca  16471  ltbwe  16523  coe1add  16647  coe1mul2lem1  16650  coe1tm  16655  xrsmcmn  16714  xrs1mnd  16726  xrs10  16727  gsumfsum  16756  zlpirlem3  16760  zlpir  16761  zcyg  16762  mulgrhm  16777  mulgrhm2  16778  zlmlmod  16794  zlmassa  16795  znbas  16814  znzrhfo  16818  zndvds  16820  frgpcyg  16844  indistopon  17055  mreclatdemo  17150  mnfnei  17275  resthauslem  17417  sshauslem  17426  discmp  17451  conima  17478  1stcfb  17498  hauseqlcld  17668  xkoptsub  17676  xkofvcn  17706  idqtop  17728  tgqtop  17734  kqdisj  17754  xpstopnlem1  17831  xpstopnlem2  17833  ufildom1  17948  alexsubb  18067  alexsubALTlem3  18070  ptcmplem2  18074  ptcmplem3  18075  tmdgsum  18115  ustneism  18243  ustuqtop1  18261  iducn  18303  prdsmet  18390  imasdsf1olem  18393  xpsxmet  18400  xpsdsval  18401  xpsmet  18402  prdsbl  18511  met1stc  18541  prdsxmslem2  18549  xpsxms  18554  xpsms  18555  dscmet  18610  nmoffn  18735  nmofval  18738  nmolb  18741  nmof  18743  cnbl0  18798  xrsmopn  18833  xrge0gsumle  18854  xrge0tsms  18855  negfcncf  18939  cnrehmeo  18968  lebnum  18979  xlebnum  18980  reparphti  19012  pcopt  19037  pcopt2  19038  pcorevcl  19040  pcorevlem  19041  pi1xfrval  19069  pi1xfrcnvlem  19071  pi1xfrcnv  19072  pi1cof  19074  pi1coval  19075  nmhmcn  19118  cphsubrglem  19130  csscld  19193  cmetcaulem  19231  cmpcmet  19260  ovolunlem1  19383  ovolicc2lem4  19406  ioorcl2  19454  uniioovol  19461  uniioombllem4  19468  uniioombllem5  19469  uniioombllem6  19470  dyadmbllem  19481  mbfsub  19544  itg1climres  19596  xrge0f  19613  itg2ge0  19617  itg2i1fseq2  19638  ibl0  19668  ellimc2  19754  limcflf  19758  dvreslem  19786  dvidlem  19792  dvid  19794  cpnres  19813  dvaddbr  19814  dvmulbr  19815  dvfre  19827  dvexp  19829  dvrec  19831  dvmptid  19833  dvmptc  19834  dvmptntr  19847  dvexp3  19852  dvlipcn  19868  dveq0  19874  dv11cn  19875  lhop2  19889  ftc1a  19911  evl1rhm  19939  evl1sca  19940  evl1var  19942  pf1mpf  19962  pf1ind  19965  tdeglem1  19971  tdeglem3  19972  tdeglem4  19973  tdeglem2  19974  mdegle0  19990  ply1remlem  20075  fta1glem2  20079  plypf1  20121  coe0  20164  dvply1  20191  elqaalem3  20228  aaliou2b  20248  aaliou3lem8  20252  aaliou3lem7  20256  taylfvallem  20264  taylf  20267  tayl0  20268  taylpfval  20271  taylply  20275  dvtaylp  20276  taylthlem1  20279  taylthlem2  20280  ulmdvlem1  20306  ulmdvlem2  20307  ulmdvlem3  20308  radcnvcl  20323  psercnlem2  20330  psercn  20332  pserdv  20335  abelthlem3  20339  abelth  20347  sincn  20350  coscn  20351  reefgim  20356  tangtx  20403  pige3  20415  cosordlem  20423  logcn  20528  dvlog  20532  advlog  20535  advlogexp  20536  logtayl  20541  logccv  20544  dvcxp1  20616  cxpcn3lem  20621  cxpcn3  20622  resqrcn  20623  sqrcn  20624  loglesqr  20632  isosctrlem2  20653  dquartlem1  20681  quart  20691  atancj  20740  efiatan  20742  atantan  20753  atanbndlem  20755  atansopn  20762  dvatan  20765  atantayl  20767  leibpilem2  20771  leibpi  20772  log2tlbnd  20775  rlimcnp2  20795  efrlim  20798  divsqrsumlem  20808  jensenlem1  20815  jensenlem2  20816  jensen  20817  amgmlem  20818  amgm  20819  emcllem4  20827  emcllem7  20830  wilthlem2  20842  wilthlem3  20843  basellem6  20858  chtrpcl  20948  ppiltx  20950  1sgm2ppw  20974  chtlepsi  20980  chpub  20994  logfacbnd3  20997  logfacrlim  20998  perfectlem2  21004  dchrelbas2  21011  dchrabs  21034  dchrhash  21045  bposlem7  21064  lgsdir2lem5  21101  lgsqrlem1  21115  lgseisenlem4  21126  lgsquad2lem1  21132  lgsquad3  21135  chpo1ub  21164  vmadivsumb  21167  rpvmasumlem  21171  dchrisumlem2  21174  dchrmusumlema  21177  dchrvmasumlem2  21182  dchrvmasumlema  21184  dchrvmasumiflem1  21185  dchrisum0flblem1  21192  dchrisum0lem1  21200  rplogsum  21211  mudivsum  21214  logdivsum  21217  mulog2sumlem2  21219  vmalogdivsum2  21222  2vmadivsumlem  21224  log2sumbnd  21228  selberglem2  21230  selbergb  21233  selberg2lem  21234  selberg2b  21236  selberg3lem1  21241  selberg4lem1  21244  selberg4  21245  pntrsumo1  21249  pntrlog2bndlem2  21262  pntrlog2bndlem3  21263  pntrlog2bndlem4  21264  pntrlog2bndlem5  21265  pntibndlem1  21273  pntibndlem2  21275  pntibndlem3  21276  pntlemb  21281  pntlemr  21286  pntlemf  21289  pntlem3  21293  pnt  21298  qabvle  21309  padicabv  21314  ostth1  21317  uhgrares  21333  umgrares  21349  usgrares  21379  nbgraop  21426  nbgraf1o0  21446  cusgra0v  21459  cusgra1v  21460  cusgraexilem2  21466  sizeusglecusg  21485  isuvtx  21487  2trllemH  21542  wlkntrllem3  21551  2wlklem1  21587  constr3trllem3  21629  constr3pthlem3  21634  vdgr0  21661  eupatrl  21680  eupares  21687  vdegp1ai  21696  vdegp1bi  21697  vsfval  22104  ipasslem7  22327  minvecolem2  22367  h2hcau  22472  h2hlm  22473  hlimadd  22685  hhsscms  22769  chocunii  22793  occllem  22795  leopnmid  23631  opsqrlem1  23633  hmopidmchi  23644  mdslj1i  23812  addltmulALT  23939  imadifxp  24028  xaddeq0  24109  xrge0npcan  24206  xrge0tsmsd  24213  xpinpreima2  24295  cnre2csqlem  24298  tpr2rico  24300  mndpluscn  24302  pnfneige0  24326  qqhghm  24362  qqhrhm  24363  qqhcn  24365  qqhucn  24366  esumsplit  24437  esumpr  24447  esumfsup  24450  sigaclcu2  24493  pwsiga  24503  prsiga  24504  measvuni  24558  elmbfmvol2  24607  mbfmcnt  24608  sxbrsigalem1  24625  sxbrsiga  24630  sibf0  24639  sitgclg  24646  isrrvv  24691  rrvadd  24700  rrvmulc  24701  dstrvprob  24719  coinflipspace  24728  coinfliprv  24730  ballotlemfmpn  24742  ballotlem1ri  24782  lgamcvg2  24829  gamcvg2lem  24833  indispcon  24911  conpcon  24912  iccllyscon  24927  cvmopnlem  24955  cvmliftlem15  24975  cvmlift2lem3  24982  circum  25101  fprodfac  25286  fallfac0  25334  bpoly4  26070  elhf2  26081  mblfinlem  26207  mblfinlem2  26208  mblfinlem3  26209  ismblfin  26210  ovoliunnfl  26211  voliunnfl  26213  volsupnfl  26214  itg2addnclem  26219  dvreasin  26243  dvreacos  26244  areacirclem2  26245  areacirclem3  26246  bnd2lem  26454  prdsbnd  26456  cntotbnd  26459  cnpwstotbnd  26460  isdrngo2  26528  prter2  26684  isnacs3  26718  diophrw  26771  lzenom  26782  diophin  26785  pellexlem5  26850  pw2f1ocnv  27062  dnnumch2  27074  kelac2lem  27094  kelac2  27095  dfac21  27096  pwssplit1  27120  uvcvv1  27170  pwfi2f1o  27192  frlmpwfi  27194  lsslinds  27233  mpaaeu  27287  rngunsnply  27310  psgnunilem5  27349  matmulr  27399  mendbas  27424  mendplusgfval  27425  mendmulrfval  27427  mendsca  27429  mendvscafval  27430  subrgacs  27440  sdrgacs  27441  cntzsdrg  27442  idomodle  27444  phisum  27450  proot1ex  27452  deg1mhm  27458  ofsubid  27473  ofdivrec  27475  dvconstbi  27483  ioovolcl  27673  stoweidlem13  27693  stoweidlem26  27706  stoweidlem34  27714  stoweidlem42  27722  stoweidlem44  27724  stoweidlem48  27728  stoweidlem62  27742  stoweid  27743  stirlinglem7  27760  stirlinglem11  27764  reumodprminv  28157  cshwoor  28167  lswrd0  28191  lswrdcshw  28193  cshwssizelem1a  28206  cshwssizensame  28216  cshwsexa  28218  usgra2wlkspthlem1  28223  usgra2wlkspthlem2  28224  frgra3v  28293  frgrancvvdeqlem9  28331  frgrancvvdgeq  28333  frg2wot1  28347  usgreghash2spotv  28356  eqlkr2  29799  tendoidcl  31467  cdlemk56  31669  dihpN  32035  mapdhval  32423  hlhillcs  32660
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator