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 5 . 2  |-  ps
43a1i 11 1  |-  ( ch 
->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6
This theorem is referenced by:  poirr2  5210  relcoi2  5353  isomin  6015  isoini  6016  supp0  6684  suppval1  6685  suppssr  6709  dmtpos  6746  oaabs2  7072  mapsncnv  7247  boxcutc  7294  domunsncan  7399  pw2f1o  7404  unxpdom2  7509  sucxpdom  7510  findcard2d  7542  ac6sfi  7544  xpfi  7571  imafi  7592  snopfsupp  7631  fifo  7670  ordtypelem4  7723  oismo  7742  wofib  7747  brwdom2  7776  canthwdom  7782  cantnffvalOLD  7859  cantnfval  7864  cantnflt  7868  cantnff  7870  cantnf0  7871  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1  7885  cantnfltOLD  7898  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1dOLD  7907  cantnflem1OLD  7908  cnfcom  7921  cnfcom2lem  7922  cnfcomOLD  7929  cnfcom2lemOLD  7930  ranksnb  8022  tskwe  8108  cardidm  8117  infxpenc  8172  infxpencOLD  8177  fseqdom  8184  dfac8clem  8190  dfac12lem2  8301  infmap2  8375  isfin4-3  8472  fin23lem14  8490  fin23lem40  8508  isf34lem7  8536  isf34lem6  8537  fin1a2lem12  8568  hsmexlem4  8586  hsmexlem5  8587  ac5b  8635  alephexp1  8731  alephsuc3  8732  axpowndlem2OLD  8751  fpwwe2lem8  8792  fpwwe2lem13  8797  canthwe  8806  canthp1lem2  8808  gchcda1  8811  pwfseqlem5  8818  wunco  8888  prlem934  9190  supsrlem  9266  msqge0  9849  ofnegsub  10308  ofsubge0  10309  xaddpnf1  11184  supxrmnf  11268  injresinjlem  11622  uzindi  11787  seqfeq4  11839  seqof  11847  bcval5  12078  hashdomi  12127  hash1snb  12155  brfi1uzind  12203  lsw0  12251  ccatlen  12259  lswccatn0lsw  12271  s111  12286  swrdspsleq  12326  wrdeqswrdlsw  12327  wrdeqs1cat  12353  reps  12392  repsw0  12399  repswccat  12407  repswrevw  12408  lswcshw  12433  cshwsexa  12442  wrdlen2i  12530  shftfib  12545  limsupcl  12935  limsupgf  12937  limsupval2  12942  isercolllem3  13128  ackbijnn  13274  supcvg  13301  ege2le3  13358  rpnnen2lem5  13484  ruclem11  13505  fsumdvds  13559  bitsinv2  13622  sadaddlem  13645  smupf  13657  smup0  13658  smu01lem  13664  isprm6  13778  hashdvds  13833  reumodprminv  13855  vdwlem13  14037  ramtlecl  14044  0ram  14064  cshwshashnsame  14113  prmlem0  14116  wunndx  14173  prdsval  14376  xpsbas  14495  xpsadd  14497  xpsmul  14498  xpssca  14499  xpsvsca  14500  xpsless  14501  xpsle  14502  mreexexlem2d  14566  mreacs  14579  acsfn  14580  idfu2nd  14770  idfucl  14774  fucsect  14865  setccatid  14935  setcepi  14939  catchomfval  14949  uncfval  15027  oduglb  15292  odumeet  15293  odulub  15294  odujoin  15295  isipodrs  15314  fpwipodrs  15317  isacs4lem  15321  isacs5lem  15322  submacs  15475  frmdup1  15522  mulgneg2  15634  subgacs  15696  nsgacs  15697  idrespermg  15896  psgnunilem5  15980  odf1o2  16052  frgpuplem  16249  cygctb  16348  gsum2dlem2  16436  gsum2dOLD  16438  dprdsubg  16495  dmdprdsplit2lem  16518  dmdprdpr  16522  dprdpr  16523  dpjeq  16532  dpjeqOLD  16539  ablfac1eulem  16547  pgpfac1lem2  16550  pgpfaclem1  16556  unitgrp  16693  isirred  16725  lssacs  16970  pwssplit1  17062  lbsextlem2  17162  lbsextlem3  17163  psrass1lem  17381  psrlidm  17408  psrlidmOLD  17409  resspsradd  17422  resspsrmul  17423  resspsrvsca  17424  ltbwe  17486  psropprmul  17591  coe1add  17616  coe1mul2lem1  17619  coe1tm  17624  xrsmcmn  17683  xrs1mnd  17695  xrs10  17696  gsumfsum  17723  zringlpir  17748  zringcyg  17749  zlpirlem3  17752  zlpir  17753  zcyg  17754  mulgrhmOLD  17771  mulgrhm2OLD  17772  zndvds  17824  regsumsupp  17894  uvcvv1  18056  lsslinds  18102  matmulr  18155  mat0dimbas0  18167  ofco2  18174  mavmul0  18205  mavmul0g  18206  mdetunilem9  18268  maducoeval2  18288  madugsum  18291  smadiadetlem0  18309  smadiadetlem1a  18311  smadiadetlem4  18317  smadiadetglem1  18319  smadiadetglem2  18320  smadiadetg  18321  cramer0  18338  indistopon  18447  mreclatdemoBAD  18542  mnfnei  18667  resthauslem  18809  sshauslem  18818  discmp  18843  conima  18871  1stcfb  18891  hauseqlcld  19061  xkoptsub  19069  xkofvcn  19099  idqtop  19121  tgqtop  19127  kqdisj  19147  xpstopnlem1  19224  xpstopnlem2  19226  ufildom1  19341  alexsubb  19460  alexsubALTlem3  19463  ptcmplem2  19467  ptcmplem3  19468  tmdgsum  19508  ustneism  19640  ustuqtop1  19658  iducn  19700  prdsmet  19787  imasdsf1olem  19790  xpsxmet  19797  xpsdsval  19798  xpsmet  19799  prdsbl  19908  met1stc  19938  prdsxmslem2  19946  xpsxms  19951  xpsms  19952  dscmet  20007  nmoffn  20132  nmofval  20135  nmolb  20138  nmof  20140  cnbl0  20195  xrsmopn  20231  xrge0gsumle  20252  xrge0tsms  20253  negfcncf  20337  cnrehmeo  20367  lebnum  20378  xlebnum  20379  reparphti  20411  pcopt  20436  pcopt2  20437  pcorevcl  20439  pcorevlem  20440  pi1xfrval  20468  pi1xfrcnvlem  20470  pi1xfrcnv  20471  pi1cof  20473  pi1coval  20474  nmhmcn  20517  cphsubrglem  20538  csscld  20603  cmetcaulem  20641  cmpcmet  20670  ovolunlem1  20822  ovolicc2lem4  20845  ioovolcl  20892  ioorcl2  20894  uniioovol  20901  uniioombllem4  20908  uniioombllem5  20909  uniioombllem6  20910  dyadmbllem  20921  mbfsub  20982  itg1climres  21034  xrge0f  21051  itg2ge0  21055  itg2i1fseq2  21076  ibl0  21106  ellimc2  21194  limcflf  21198  dvreslem  21226  dvidlem  21232  dvid  21234  cpnres  21253  dvaddbr  21254  dvmulbr  21255  dvfre  21267  dvexp  21269  dvrec  21271  dvmptid  21273  dvmptc  21274  dvmptntr  21287  dvexp3  21292  dvlipcn  21308  dveq0  21314  dv11cn  21315  lhop2  21329  ftc1a  21351  evl1rhm  21380  evl1sca  21381  evl1var  21383  pf1mpf  21403  pf1ind  21406  tdeglem1  21412  tdeglem3  21413  tdeglem4  21414  tdeglem2  21415  mdeg0  21426  mdegle0  21433  ply1remlem  21519  fta1glem2  21523  plypf1  21565  coe0  21608  dvply1  21635  elqaalem3  21672  aaliou2b  21692  aaliou3lem8  21696  aaliou3lem7  21700  taylfvallem  21708  taylf  21711  tayl0  21712  taylpfval  21715  taylply  21719  dvtaylp  21720  taylthlem1  21723  taylthlem2  21724  ulmdvlem1  21750  ulmdvlem2  21751  ulmdvlem3  21752  radcnvcl  21767  psercnlem2  21774  psercn  21776  pserdv  21779  abelthlem3  21783  abelth  21791  sincn  21794  coscn  21795  reefgim  21800  tangtx  21852  pige3  21864  cosordlem  21872  logcn  21977  dvlog  21981  advlog  21984  advlogexp  21985  logtayl  21990  logccv  21993  dvcxp1  22065  cxpcn3lem  22070  cxpcn3  22071  resqrcn  22072  sqrcn  22073  loglesqr  22081  isosctrlem2  22102  dquartlem1  22131  quart  22141  atancj  22190  efiatan  22192  atantan  22203  atanbndlem  22205  atansopn  22212  dvatan  22215  atantayl  22217  leibpilem2  22221  leibpi  22222  log2tlbnd  22225  rlimcnp2  22245  efrlim  22248  divsqrsumlem  22258  jensenlem1  22265  jensenlem2  22266  jensen  22267  amgmlem  22268  amgm  22269  emcllem4  22277  emcllem7  22280  wilthlem2  22292  wilthlem3  22293  basellem6  22308  chtrpcl  22398  ppiltx  22400  1sgm2ppw  22424  chtlepsi  22430  chpub  22444  logfacbnd3  22447  logfacrlim  22448  perfectlem2  22454  dchrelbas2  22461  dchrabs  22484  dchrhash  22495  bposlem7  22514  lgsdir2lem5  22551  lgsqrlem1  22565  lgseisenlem4  22576  lgsquad2lem1  22582  lgsquad3  22585  chpo1ub  22614  vmadivsumb  22617  rpvmasumlem  22621  dchrisumlem2  22624  dchrmusumlema  22627  dchrvmasumlem2  22632  dchrvmasumlema  22634  dchrvmasumiflem1  22635  dchrisum0flblem1  22642  dchrisum0lem1  22650  rplogsum  22661  mudivsum  22664  logdivsum  22667  mulog2sumlem2  22669  vmalogdivsum2  22672  2vmadivsumlem  22674  log2sumbnd  22678  selberglem2  22680  selbergb  22683  selberg2lem  22684  selberg2b  22686  selberg3lem1  22691  selberg4lem1  22694  selberg4  22695  pntrsumo1  22699  pntrlog2bndlem2  22712  pntrlog2bndlem3  22713  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntibndlem1  22723  pntibndlem2  22725  pntibndlem3  22726  pntlemb  22731  pntlemr  22736  pntlemf  22739  pntlem3  22743  pnt  22748  qabvle  22759  padicabv  22764  ostth1  22767  uhgrares  23065  umgrares  23081  usgrares  23111  nbgraop  23158  nbgraf1o0  23178  cusgra0v  23191  cusgra1v  23192  cusgraexilem2  23198  sizeusglecusg  23217  isuvtx  23219  2trllemH  23274  wlkntrllem3  23283  2wlklem1  23319  constr3trllem3  23361  constr3pthlem3  23366  vdgr0  23393  eupatrl  23412  eupares  23419  vdegp1ai  23428  vdegp1bi  23429  vsfval  23836  ipasslem7  24059  minvecolem2  24099  h2hcau  24204  h2hlm  24205  hlimadd  24418  hhsscms  24503  chocunii  24527  occllem  24529  leopnmid  25365  opsqrlem1  25367  hmopidmchi  25378  mdslj1i  25546  addltmulALT  25673  imadifxp  25763  xaddeq0  25871  xrge0npcan  25981  xrge0tsmsd  26106  xpinpreima2  26191  cnre2csqlem  26194  tpr2rico  26196  ordtrestNEW  26205  mndpluscn  26210  pnfneige0  26235  qqhghm  26271  qqhrhm  26272  qqhcn  26274  qqhucn  26275  rrhre  26301  esumsplit  26360  esumpr  26370  esumfsup  26373  sigaclcu2  26417  pwsiga  26427  prsiga  26428  measvuni  26482  elmbfmvol2  26536  mbfmcnt  26537  sxbrsigalem1  26554  sxbrsiga  26559  sibf0  26568  sitgclg  26576  eulerpartgbij  26603  eulerpartlemgh  26609  isrrvv  26674  rrvadd  26683  rrvmulc  26684  dstrvprob  26702  coinflipspace  26711  coinfliprv  26713  ballotlemfmpn  26725  ballotlem1ri  26765  signsplypnf  26799  signsply0  26800  signswrid  26807  lgamcvg2  26889  gamcvg2lem  26893  indispcon  26971  conpcon  26972  iccllyscon  26987  cvmopnlem  27015  cvmliftlem15  27035  cvmlift2lem3  27042  circum  27166  fprodfac  27330  fallfac0  27378  bpoly4  28049  elhf2  28060  finixpnum  28258  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  dvtan  28286  itg2addnclem  28287  ftc1anclem5  28315  dvcncxp1  28321  dvasin  28324  dvreasin  28326  dvreacos  28327  areacirclem1  28328  areacirc  28333  bnd2lem  28534  prdsbnd  28536  cntotbnd  28539  cnpwstotbnd  28540  isdrngo2  28608  prter2  28871  isnacs3  28891  diophrw  28942  lzenom  28953  diophin  28956  pellexlem5  29019  pw2f1ocnv  29231  dnnumch2  29243  kelac2lem  29262  kelac2  29263  dfac21  29264  pwfi2f1o  29296  frlmpwfi  29298  mpaaeu  29352  rngunsnply  29375  mendbas  29386  mendplusgfval  29387  mendmulrfval  29389  mendsca  29391  mendvscafval  29392  subrgacs  29402  sdrgacs  29403  cntzsdrg  29404  idomodle  29406  phisum  29412  proot1ex  29414  deg1mhm  29420  itgpowd  29435  ofsubid  29443  ofdivrec  29445  dvconstbi  29453  stoweidlem13  29654  stoweidlem26  29667  stoweidlem34  29675  stoweidlem42  29683  stoweidlem44  29685  stoweidlem48  29689  stoweidlem62  29703  stoweid  29704  stirlinglem7  29721  stirlinglem11  29725  fvelrnfvelrnressn  29997  modfsummods  30090  lswccats1fst  30108  usg2wlkeq  30135  usgra2wlkspthlem1  30142  usgra2wlkspthlem2  30143  wwlkn  30162  wlkiswwlk2  30177  wwlkn0s  30185  wwlkexthasheq  30212  wlknwwlknvbij  30218  clwwlkn  30276  clwwlkn2  30284  clwlkisclwwlklem2  30294  clwwlkvbij  30309  scshwfzeqfzo  30338  eclclwwlkn0  30351  hashecclwwlkn1  30354  usghashecclwwlk  30355  rusgrasn  30403  frgra3v  30440  frgrancvvdeqlem9  30480  frgrancvvdgeq  30482  frg2wot1  30496  usgreghash2spotv  30505  extwwlkfablem2  30517  numclwwlkovf2  30523  numclwwlk2lem3  30545  zlmodzxzel  30586  zlmodzxzsubm  30590  zlmodzxzsub  30591  gsumpr  30592  psgnsn  30602  isnzr2hash  30605  scmsuppss  30616  lcoop  30654  lincval0  30658  lco0  30670  linds0  30708  snlindsntorlem  30713  rng1nnzr  30735  lmod1lem2  30739  lmod1lem3  30740  lmod1zr  30744  lmod1zrnlvec  30745  zlmodzxznm  30748  zlmodzxzldeplem4  30754  eqlkr2  32318  tendoidcl  33986  cdlemk56  34188  dihpN  34554  mapdhval  34942  hlhillcs  35179
  Copyright terms: Public domain W3C validator