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  5217  relcoi2  5356  isomin  6016  isoini  6017  dmtpos  6450  oaabs2  6847  mapsncnv  7019  boxcutc  7064  domunsncan  7167  pw2f1o  7172  unxpdom2  7276  sucxpdom  7277  ac6sfi  7310  xpfi  7337  imafi  7357  fifo  7395  ordtypelem4  7446  oismo  7465  wofib  7470  brwdom2  7497  canthwdom  7503  cantnflt  7583  cantnff  7585  cantnf0  7586  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  cnfcom  7613  cnfcom2lem  7614  ranksnb  7709  tskwe  7793  cardidm  7802  infxpenc  7855  fseqdom  7863  dfac8clem  7869  dfac12lem2  7980  infmap2  8054  isfin4-3  8151  fin23lem14  8169  fin23lem40  8187  isf34lem7  8215  isf34lem6  8216  fin1a2lem12  8247  hsmexlem4  8265  hsmexlem5  8266  ac5b  8314  alephexp1  8410  alephsuc3  8411  axpowndlem2  8429  fpwwe2lem8  8468  fpwwe2lem13  8473  canthwe  8482  canthp1lem2  8484  gchcda1  8487  pwfseqlem5  8494  wunco  8564  prlem934  8866  supsrlem  8942  msqge0  9505  ofnegsub  9954  ofsubge0  9955  xaddpnf1  10768  supxrmnf  10852  injresinjlem  11154  uzindi  11275  seqfeq4  11327  seqof  11335  bcval5  11564  hashdomi  11609  hash1snb  11636  brfi1uzind  11670  ccatlen  11699  s111  11717  wrdeqs1cat  11744  shftfib  11842  limsupcl  12222  limsupgf  12224  limsupval2  12229  isercolllem3  12415  ackbijnn  12562  supcvg  12590  ege2le3  12647  rpnnen2lem5  12773  ruclem11  12794  fsumdvds  12848  bitsinv2  12910  sadaddlem  12933  smupf  12945  smup0  12946  smu01lem  12952  isprm6  13064  hashdvds  13119  vdwlem13  13316  ramtlecl  13323  0ram  13343  prmlem0  13383  wunndx  13440  prdsval  13633  xpsbas  13754  xpsadd  13756  xpsmul  13757  xpssca  13758  xpsvsca  13759  xpsless  13760  xpsle  13761  mreexexlem2d  13825  mreacs  13838  acsfn  13839  idfu2nd  14029  idfucl  14033  fucsect  14124  setccatid  14194  setcepi  14198  catchomfval  14208  uncfval  14286  oduglb  14521  odumeet  14522  odulub  14523  odujoin  14524  isipodrs  14542  fpwipodrs  14545  isacs4lem  14549  isacs5lem  14550  submacs  14720  frmdup1  14764  mulgneg2  14872  subgacs  14930  nsgacs  14931  odf1o2  15162  frgpuplem  15359  cygctb  15456  gsum2d  15501  dprdsubg  15537  dmdprdsplit2lem  15558  dmdprdpr  15562  dprdpr  15563  dpjeq  15572  ablfac1eulem  15585  pgpfac1lem2  15588  pgpfaclem1  15594  unitgrp  15727  isirred  15759  lssacs  15998  lbsextlem2  16186  lbsextlem3  16187  psrlidm  16422  resspsradd  16434  resspsrmul  16435  resspsrvsca  16436  ltbwe  16488  coe1add  16612  coe1mul2lem1  16615  coe1tm  16620  xrsmcmn  16679  xrs1mnd  16691  xrs10  16692  gsumfsum  16721  zlpirlem3  16725  zlpir  16726  zcyg  16727  mulgrhm  16742  mulgrhm2  16743  zlmlmod  16759  zlmassa  16760  znbas  16779  znzrhfo  16783  zndvds  16785  frgpcyg  16809  indistopon  17020  mreclatdemo  17115  mnfnei  17239  resthauslem  17381  sshauslem  17390  discmp  17415  conima  17441  1stcfb  17461  hauseqlcld  17631  xkoptsub  17639  xkofvcn  17669  idqtop  17691  tgqtop  17697  kqdisj  17717  xpstopnlem1  17794  xpstopnlem2  17796  ufildom1  17911  alexsubb  18030  alexsubALTlem3  18033  ptcmplem2  18037  ptcmplem3  18038  tmdgsum  18078  ustneism  18206  ustuqtop1  18224  iducn  18266  prdsmet  18353  imasdsf1olem  18356  xpsxmet  18363  xpsdsval  18364  xpsmet  18365  prdsbl  18474  met1stc  18504  prdsxmslem2  18512  xpsxms  18517  xpsms  18518  dscmet  18573  nmoffn  18698  nmofval  18701  nmolb  18704  nmof  18706  cnbl0  18761  xrsmopn  18796  xrge0gsumle  18817  xrge0tsms  18818  negfcncf  18902  cnrehmeo  18931  lebnum  18942  xlebnum  18943  reparphti  18975  pcopt  19000  pcopt2  19001  pcorevcl  19003  pcorevlem  19004  pi1xfrval  19032  pi1xfrcnvlem  19034  pi1xfrcnv  19035  pi1cof  19037  pi1coval  19038  nmhmcn  19081  cphsubrglem  19093  csscld  19156  cmetcaulem  19194  cmpcmet  19223  ovolunlem1  19346  ovolicc2lem4  19369  ioorcl2  19417  uniioovol  19424  uniioombllem4  19431  uniioombllem5  19432  uniioombllem6  19433  dyadmbllem  19444  mbfsub  19507  itg1climres  19559  xrge0f  19576  itg2ge0  19580  itg2i1fseq2  19601  ibl0  19631  ellimc2  19717  limcflf  19721  dvreslem  19749  dvidlem  19755  dvid  19757  cpnres  19776  dvaddbr  19777  dvmulbr  19778  dvfre  19790  dvexp  19792  dvrec  19794  dvmptid  19796  dvmptc  19797  dvmptntr  19810  dvexp3  19815  dvlipcn  19831  dveq0  19837  dv11cn  19838  lhop2  19852  ftc1a  19874  evl1rhm  19902  evl1sca  19903  evl1var  19905  pf1mpf  19925  pf1ind  19928  tdeglem1  19934  tdeglem3  19935  tdeglem4  19936  tdeglem2  19937  mdegle0  19953  ply1remlem  20038  fta1glem2  20042  plypf1  20084  coe0  20127  dvply1  20154  elqaalem3  20191  aaliou2b  20211  aaliou3lem8  20215  aaliou3lem7  20219  taylfvallem  20227  taylf  20230  tayl0  20231  taylpfval  20234  taylply  20238  dvtaylp  20239  taylthlem1  20242  taylthlem2  20243  ulmdvlem1  20269  ulmdvlem2  20270  ulmdvlem3  20271  radcnvcl  20286  psercnlem2  20293  psercn  20295  pserdv  20298  abelthlem3  20302  abelth  20310  sincn  20313  coscn  20314  reefgim  20319  tangtx  20366  pige3  20378  cosordlem  20386  logcn  20491  dvlog  20495  advlog  20498  advlogexp  20499  logtayl  20504  logccv  20507  dvcxp1  20579  cxpcn3lem  20584  cxpcn3  20585  resqrcn  20586  sqrcn  20587  loglesqr  20595  isosctrlem2  20616  dquartlem1  20644  quart  20654  atancj  20703  efiatan  20705  atantan  20716  atanbndlem  20718  atansopn  20725  dvatan  20728  atantayl  20730  leibpilem2  20734  leibpi  20735  log2tlbnd  20738  rlimcnp2  20758  efrlim  20761  divsqrsumlem  20771  jensenlem1  20778  jensenlem2  20779  jensen  20780  amgmlem  20781  amgm  20782  emcllem4  20790  emcllem7  20793  wilthlem2  20805  wilthlem3  20806  basellem6  20821  chtrpcl  20911  ppiltx  20913  1sgm2ppw  20937  chtlepsi  20943  chpub  20957  logfacbnd3  20960  logfacrlim  20961  perfectlem2  20967  dchrelbas2  20974  dchrabs  20997  dchrhash  21008  bposlem7  21027  lgsdir2lem5  21064  lgsqrlem1  21078  lgseisenlem4  21089  lgsquad2lem1  21095  lgsquad3  21098  chpo1ub  21127  vmadivsumb  21130  rpvmasumlem  21134  dchrisumlem2  21137  dchrmusumlema  21140  dchrvmasumlem2  21145  dchrvmasumlema  21147  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  dchrisum0lem1  21163  rplogsum  21174  mudivsum  21177  logdivsum  21180  mulog2sumlem2  21182  vmalogdivsum2  21185  2vmadivsumlem  21187  log2sumbnd  21191  selberglem2  21193  selbergb  21196  selberg2lem  21197  selberg2b  21199  selberg3lem1  21204  selberg4lem1  21207  selberg4  21208  pntrsumo1  21212  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntibndlem1  21236  pntibndlem2  21238  pntibndlem3  21239  pntlemb  21244  pntlemr  21249  pntlemf  21252  pntlem3  21256  pnt  21261  qabvle  21272  padicabv  21277  ostth1  21280  uhgrares  21296  umgrares  21312  usgrares  21342  nbgraop  21389  nbgraf1o0  21409  cusgra0v  21422  cusgra1v  21423  cusgraexilem2  21429  sizeusglecusg  21448  isuvtx  21450  2trllemH  21505  wlkntrllem3  21514  2wlklem1  21550  constr3trllem3  21592  constr3pthlem3  21597  vdgr0  21624  eupatrl  21643  eupares  21650  vdegp1ai  21659  vdegp1bi  21660  vsfval  22067  ipasslem7  22290  minvecolem2  22330  h2hcau  22435  h2hlm  22436  hlimadd  22648  hhsscms  22732  chocunii  22756  occllem  22758  leopnmid  23594  opsqrlem1  23596  hmopidmchi  23607  mdslj1i  23775  addltmulALT  23902  imadifxp  23991  xaddeq0  24072  xrge0npcan  24169  xrge0tsmsd  24176  xpinpreima2  24258  cnre2csqlem  24261  tpr2rico  24263  mndpluscn  24265  pnfneige0  24289  qqhghm  24325  qqhrhm  24326  qqhcn  24328  qqhucn  24329  esumsplit  24400  esumpr  24410  esumfsup  24413  sigaclcu2  24456  pwsiga  24466  prsiga  24467  measvuni  24521  elmbfmvol2  24570  mbfmcnt  24571  sxbrsigalem1  24588  sxbrsiga  24593  sibf0  24602  sitgclg  24609  isrrvv  24654  rrvadd  24663  rrvmulc  24664  dstrvprob  24682  coinflipspace  24691  coinfliprv  24693  ballotlemfmpn  24705  ballotlem1ri  24745  lgamcvg2  24792  gamcvg2lem  24796  indispcon  24874  conpcon  24875  iccllyscon  24890  cvmopnlem  24918  cvmliftlem15  24938  cvmlift2lem3  24945  circum  25064  fprodfac  25249  fallfac0  25296  bpoly4  26009  elhf2  26020  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  itg2addnclem  26155  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem3  26182  bnd2lem  26390  prdsbnd  26392  cntotbnd  26395  cnpwstotbnd  26396  isdrngo2  26464  prter2  26620  isnacs3  26654  diophrw  26707  lzenom  26718  diophin  26721  pellexlem5  26786  pw2f1ocnv  26998  dnnumch2  27010  kelac2lem  27030  kelac2  27031  dfac21  27032  pwssplit1  27056  uvcvv1  27106  pwfi2f1o  27128  frlmpwfi  27130  lsslinds  27169  mpaaeu  27223  rngunsnply  27246  psgnunilem5  27285  matmulr  27335  mendbas  27360  mendplusgfval  27361  mendmulrfval  27363  mendsca  27365  mendvscafval  27366  subrgacs  27376  sdrgacs  27377  cntzsdrg  27378  idomodle  27380  phisum  27386  proot1ex  27388  deg1mhm  27394  ofsubid  27409  ofdivrec  27411  dvconstbi  27419  ioovolcl  27609  stoweidlem13  27629  stoweidlem26  27642  stoweidlem34  27650  stoweidlem42  27658  stoweidlem44  27660  stoweidlem48  27664  stoweidlem62  27678  stoweid  27679  stirlinglem7  27696  stirlinglem11  27700  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  frgra3v  28106  frgrancvvdeqlem9  28144  frgrancvvdgeq  28146  frg2wot1  28160  usgreghash2spotv  28169  eqlkr2  29583  tendoidcl  31251  cdlemk56  31453  dihpN  31819  mapdhval  32207  hlhillcs  32444
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator