Theorem mp1i 13

Description: Inference detaching an antecedent and introducing a new one. (Contributed by Stefan O'Rear, 29-Jan-2015.)

Hypotheses

Ref	Expression
mp1i.1	|- ph
mp1i.2	|- ( ph -> ps )

Assertion

Ref	Expression
mp1i	|- ( ch -> ps )

Proof of Theorem mp1i

Step	Hyp	Ref	Expression
1		mp1i.1	. . 3 |- ph
2		mp1i.2	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4	3	a1i 11	1 |- ( ch -> ps )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  poirr2  5520  fvrnressn  6428  isomin  6587  isoini  6588  mptmpt2opabbrd  7248  supp0  7300  suppval1  7301  suppssr  7326  dmtpos  7364  mpt2curryd  7395  oaabs2  7725  elqsecl  7801  mapsncnv  7904  boxcutc  7951  domunsncan  8060  unxpdom2  8168  sucxpdom  8169  findcard2d  8202  ac6sfi  8204  xpfi  8231  imafi  8259  snopfsupp  8298  fifo  8338  ordtypelem4  8426  oismo  8445  wofib  8450  brwdom2  8478  canthwdom  8484  cantnfval  8565  cantnflt  8569  cantnff  8571  cantnf0  8572  cantnfp1lem1  8575  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1  8586  cnfcom  8597  cnfcom2lem  8598  ranksnb  8690  tskwe  8776  cardidm  8785  infxpenc  8841  fseqdom  8849  dfac8clem  8855  dfac12lem2  8966  infmap2  9040  isfin4-3  9137  fin23lem14  9155  fin23lem40  9173  isf34lem7  9201  isf34lem6  9202  fin1a2lem12  9233  hsmexlem4  9251  hsmexlem5  9252  ac5b  9300  alephexp1  9401  alephsuc3  9402  fpwwe2lem8  9459  fpwwe2lem13  9464  canthwe  9473  canthp1lem2  9475  gchcda1  9478  pwfseqlem5  9485  wunco  9555  prlem934  9855  supsrlem  9932  msqge0  10549  negfi  10971  ofnegsub  11018  ofsubge0  11019  xaddpnf1  12057  supxrmnf  12147  fz0sn0fz1  12456  injresinjlem  12588  fldiv4lem1div2  12638  uzindi  12781  seqfeq4  12850  seqof  12858  bcval5  13105  hashdomi  13169  hash1snb  13207  hashge2el2difr  13263  hashtpg  13267  fi1uzind  13279  fi1uzindOLD  13285  ccatlen  13360  lswccatn0lsw  13373  ccatalpha  13375  eqs1  13392  s111  13395  swrd0  13434  swrdspsleq  13449  wrdeqs1cat  13474  reps  13517  repsw0  13524  repswccat  13532  repswrevw  13533  lswcshw  13561  cshwsexa  13570  scshwfzeqfzo  13572  lsws2  13649  lsws3  13650  lsws4  13651  wrdlen2i  13686  relexpsucnnr  13765  relexpaddg  13793  shftfib  13812  limsupcl  14204  limsupgf  14206  limsupval2  14211  isercolllem3  14397  modfsummods  14525  ackbijnn  14560  supcvg  14588  fprodfac  14703  fprodmodd  14728  fallfac0  14759  bpoly4  14790  ege2le3  14820  rpnnen2lem5  14947  ruclem11  14969  fsumdvds  15030  fproddvdsd  15059  mod2eq1n2dvds  15071  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  bitsinv2  15165  sadaddlem  15188  smupf  15200  smup0  15201  smu01lem  15207  3lcm2e6woprm  15328  6lcm4e12  15329  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  coprmprod  15375  isprm6  15426  hashdvds  15480  phisum  15495  reumodprminv  15509  prmreclem6  15625  vdwlem13  15697  ramtlecl  15704  0ram  15724  prmdvdsprmo  15746  fvprmselgcd1  15749  prmgaplcmlem1  15755  prmgaplem7  15761  prmgaplcm  15764  cshwshashnsame  15810  prmlem0  15812  wunndx  15878  prdsval  16115  xpsbas  16234  xpsadd  16236  xpsmul  16237  xpssca  16238  xpsvsca  16239  xpsless  16240  xpsle  16241  mreexexlem2d  16305  mreacs  16319  acsfn  16320  isofn  16435  ciclcl  16462  cicrcl  16463  cicsym  16464  cicer  16466  idfu2nd  16537  idfucl  16541  fucsect  16632  initoeu2lem1  16664  initoeu2lem2  16665  setccatid  16734  setcepi  16738  catchomfval  16748  estrccatid  16772  estrreslem1  16777  estrreslem2  16778  estrres  16779  funcestrcsetclem8  16787  fullestrcsetc  16791  embedsetcestrclem  16797  funcsetcestrclem8  16802  uncfval  16874  oduglb  17139  odumeet  17140  odulub  17141  odujoin  17142  isipodrs  17161  fpwipodrs  17164  isacs5lem  17169  idmhm  17344  submacs  17365  frmdup1  17401  mgmnsgrpex  17418  mulgneg2  17575  subgacs  17629  nsgacs  17630  idrespermg  17831  psgnunilem5  17914  psgnsn  17940  odf1o2  17988  frgpuplem  18185  cygctb  18293  gsumzunsnd  18355  gsum2dlem2  18370  gsummptnn0fz  18382  dprdsubg  18423  dmdprdsplit2lem  18444  dmdprdpr  18448  dprdpr  18449  dpjeq  18458  ablfac1eulem  18471  pgpfac1lem2  18474  pgpfaclem1  18480  srgbinomlem4  18543  unitgrp  18667  isirred  18699  brric  18744  mptscmfsupp0  18928  lssacs  18967  pwssplit1  19059  lbsextlem2  19159  lbsextlem3  19160  isnzr2hash  19264  0ring01eqbi  19273  rng1nnzr  19274  psrass1lem  19377  psrlidm  19403  resspsradd  19416  resspsrmul  19417  resspsrvsca  19418  mplcoe5lem  19467  ltbwe  19472  coe1fsupp  19584  psropprmul  19608  coe1add  19634  coe1mul2lem1  19637  coe1tm  19643  cply1coe0bi  19670  evls1rhmlem  19686  evl1sca  19698  evl1var  19700  pf1mpf  19716  pf1ind  19719  xrsmcmn  19769  xrs1mnd  19784  xrs10  19785  gsumfsum  19813  zringlpir  19837  zringcyg  19839  zndvds  19898  regsumsupp  19968  uvcvv1  20128  lsslinds  20170  matmulr  20244  ofco2  20257  mat0dimbas0  20272  mat1dimelbas  20277  mat1f1o  20284  dmatval  20298  scmatghm  20339  mavmul0  20358  mavmul0g  20359  m1detdiag  20403  mdetunilem9  20426  maducoeval2  20446  madugsum  20449  smadiadetlem0  20467  smadiadetlem1a  20469  smadiadetlem4  20475  smadiadetglem1  20477  smadiadetglem2  20478  smadiadetg  20479  cramer0  20496  cpmat  20514  mat2pmatfval  20528  cpm2mfval  20554  m2cpminvid2lem  20559  pmatcollpw3fi1lem2  20592  pmatcollpw3fi1  20593  idpm2idmp  20606  pm2mpmhmlem2  20624  chpmatfval  20635  chfacfscmulfsupp  20664  chfacfpmmulfsupp  20668  cpmidpmatlem2  20676  cpmadugsumlemF  20681  cpmidgsum2  20684  cpmadumatpolylem1  20686  cayhamlem3  20692  cayhamlem4  20693  indistopon  20805  mreclatdemoBAD  20900  mnfnei  21025  resthauslem  21167  sshauslem  21176  discmp  21201  connima  21228  1stcfb  21248  ptbasfi  21384  hauseqlcld  21449  xkoptsub  21457  xkofvcn  21487  idqtop  21509  tgqtop  21515  kqdisj  21535  xpstopnlem1  21612  xpstopnlem2  21614  ufildom1  21730  alexsubb  21850  alexsubALTlem3  21853  ptcmplem2  21857  ptcmplem3  21858  tmdgsum  21899  ustneism  22027  ustuqtop1  22045  iducn  22087  prdsmet  22175  imasdsf1olem  22178  xpsxmet  22185  xpsdsval  22186  xpsmet  22187  prdsbl  22296  met1stc  22326  prdsxmslem2  22334  xpsxms  22339  xpsms  22340  psmetutop  22372  dscmet  22377  nmoffn  22515  nmofval  22518  nmolb  22521  nmof  22523  cnbl0  22577  xrsmopn  22615  xrge0gsumle  22636  xrge0tsms  22637  negfcncf  22722  cnrehmeo  22752  lebnum  22763  xlebnum  22764  reparphti  22797  pcopt  22822  pcopt2  22823  pcorevcl  22825  pcorevlem  22826  pi1xfrval  22854  pi1xfrcnvlem  22856  pi1xfrcnv  22857  pi1cof  22859  pi1coval  22860  nmhmcn  22920  cphsubrglem  22977  csscld  23048  cmetcaulem  23086  cmpcmet  23116  divcncf  23216  ovolunlem1  23265  ovolicc2lem4  23288  ioovolcl  23338  ioorcl2  23340  uniioovol  23347  uniioombllem4  23354  uniioombllem5  23355  uniioombllem6  23356  dyadmbllem  23367  mbfsub  23429  itg1climres  23481  xrge0f  23498  itg2ge0  23502  itg2i1fseq2  23523  ibl0  23553  ellimc2  23641  limcflf  23645  dvreslem  23673  dvidlem  23679  dvid  23681  cpnres  23700  dvaddbr  23701  dvmulbr  23702  dvfre  23714  dvexp  23716  dvrec  23718  dvmptid  23720  dvmptc  23721  dvmptntr  23734  dvexp3  23741  dvlipcn  23757  dveq0  23763  dv11cn  23764  lhop2  23778  ftc1a  23800  tdeglem1  23818  tdeglem3  23819  tdeglem4  23820  tdeglem2  23821  mdeg0  23830  mdegle0  23837  ply1remlem  23922  plypf1  23968  coe0  24012  dvply1  24039  elqaalem3  24076  aaliou2b  24096  aaliou3lem8  24100  aaliou3lem7  24104  taylfvallem  24112  taylf  24115  tayl0  24116  taylpfval  24119  taylply  24123  dvtaylp  24124  taylthlem1  24127  taylthlem2  24128  ulmdvlem1  24154  ulmdvlem2  24155  ulmdvlem3  24156  radcnvcl  24171  psercnlem2  24178  psercn  24180  pserdv  24183  abelthlem3  24187  abelth  24195  sincn  24198  coscn  24199  reefgim  24204  tangtx  24257  pige3  24269  cosordlem  24277  logcn  24393  dvlog  24397  advlog  24400  advlogexp  24401  logtayl  24406  logccv  24409  dvcxp1  24481  dvcncxp1  24484  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  sqrtcn  24491  loglesqrt  24499  logbfval  24528  logblog  24530  isosctrlem2  24549  dquartlem1  24578  quart  24588  atancj  24637  efiatan  24639  atantan  24650  atanbndlem  24652  atansopn  24659  dvatan  24662  atantayl  24664  leibpilem2  24668  leibpi  24669  log2tlbnd  24672  rlimcnp2  24693  efrlim  24696  divsqrtsumlem  24706  jensenlem1  24713  jensenlem2  24714  jensen  24715  amgmlem  24716  amgm  24717  emcllem4  24725  emcllem7  24728  lgamcvg2  24781  gamcvg2lem  24785  wilthlem2  24795  wilthlem3  24796  basellem6  24812  chtrpcl  24901  ppiltx  24903  1sgm2ppw  24925  chtlepsi  24931  chpub  24945  logfacbnd3  24948  logfacrlim  24949  perfectlem2  24955  dchrelbas2  24962  dchrabs  24985  dchrhash  24996  bposlem7  25015  lgsdir2lem5  25054  lgsqrlem1  25071  gausslemma2dlem5  25096  gausslemma2dlem6  25097  lgseisenlem4  25103  lgsquad2lem1  25109  lgsquad3  25112  chpo1ub  25169  vmadivsumb  25172  rpvmasumlem  25176  dchrisumlem2  25179  dchrmusumlema  25182  dchrvmasumlem2  25187  dchrvmasumlema  25189  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0lem1  25205  rplogsum  25216  mudivsum  25219  logdivsum  25222  mulog2sumlem2  25224  vmalogdivsum2  25227  2vmadivsumlem  25229  log2sumbnd  25233  selberglem2  25235  selbergb  25238  selberg2lem  25239  selberg2b  25241  selberg3lem1  25246  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntibndlem1  25278  pntibndlem2  25280  pntibndlem3  25281  pntlemb  25286  pntlemr  25291  pntlemf  25294  pntlem3  25298  pnt  25303  qabvle  25314  padicabv  25319  ostth1  25322  istrkg2ld  25359  tgldimor  25397  tgcgr4  25426  motgrp  25438  perpln1  25605  perpln2  25606  isperp  25607  snstrvtxval  25929  snstriedgval  25930  isuhgrop  25965  uhgrunop  25970  uhgrstrrepe  25973  upgrop  25989  upgrunop  26014  umgrunop  26016  isusgrs  26051  isuspgrop  26056  isusgrop  26057  usgrop  26058  usgrstrrepe  26127  uspgr1ewop  26140  usgr2v1e2w  26144  uhgrspan1  26195  upgrres  26198  umgrres  26199  usgrres  26200  upgrres1  26205  umgrres1  26206  usgrres1  26207  isfusgrcl  26213  fusgredgfi  26217  usgr1v0e  26218  nbgrval  26234  nbusgrf1o1  26272  nbfusgrlevtxm2  26280  uvtxa01vtx0  26297  nbupgruvtxres  26308  usgrexilem  26336  usgrexi  26337  cusgrexi  26339  structtousgr  26341  structtocusgr  26342  cusgrres  26344  cusgrfilem3  26353  sizusglecusg  26359  vtxdgfval  26363  vtxdgop  26366  vtxdgf  26367  vtxdlfgrval  26381  vtxd0nedgb  26384  vtxdusgr0edgnelALT  26392  1loopgrvd0  26400  1egrvtxdg1  26405  1egrvtxdg0  26407  p1evtxdeqlem  26408  p1evtxdeq  26409  p1evtxdp1  26410  umgr2v2e  26421  vdiscusgrb  26426  vdegp1ai  26432  vdegp1bi  26433  ewlkle  26501  wksfval  26505  wksv  26515  wlk1ewlk  26536  uspgr2wlkeq  26542  wlkp1lem8  26577  upgr2pthnlp  26628  wlkiswwlks2  26761  wlksnwwlknvbij  26803  wwlksnextproplem1  26804  2pthdlem1  26826  elwwlks2  26861  clwlkclwwlklem1  26900  clwwlksnfi  26913  clwwlksvbij  26922  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  0wlkonlem1  26979  0wlkons1  26982  0pthon  26988  3wlkdlem4  27022  upgr3v3e3cycl  27040  trlsegvdeglem3  27082  trlsegvdeglem5  27084  eupth2lemb  27097  frgr3v  27139  frgr2wwlk1  27193  fusgreghash2wspv  27199  ex-lcm  27315  vsfval  27488  ipasslem7  27691  minvecolem2  27731  h2hcau  27836  h2hlm  27837  hlimadd  28050  hhsscms  28136  chocunii  28160  occllem  28162  leopnmid  28997  opsqrlem1  28999  hmopidmchi  29010  mdslj1i  29178  addltmulALT  29305  imadifxp  29414  xaddeq0  29518  fzodif2  29552  xrge0npcan  29694  gsumle  29779  xrge0tsmsd  29785  locfinreflem  29907  locfinref  29908  xpinpreima2  29953  cnre2csqlem  29956  tpr2rico  29958  ordtrestNEW  29967  ordtrest2NEW  29969  mndpluscn  29972  pnfneige0  29997  qqhghm  30032  qqhrhm  30033  qqhcn  30035  qqhucn  30036  rrhcn  30041  rrhre  30065  esumsplit  30115  esumpr  30128  esumfsup  30132  sigaclcu2  30183  pwsiga  30193  prsiga  30194  sigapildsys  30225  ldgenpisyslem1  30226  measvuni  30277  elmbfmvol2  30329  mbfmcnt  30330  sxbrsigalem1  30347  sxbrsiga  30352  omsfval  30356  carsgclctunlem2  30381  sibf0  30396  sitgclg  30404  sitmval  30411  eulerpartgbij  30434  eulerpartlemgh  30440  isrrvv  30505  rrvadd  30514  rrvmulc  30515  dstrvprob  30533  coinflipspace  30542  coinfliprv  30544  ballotlemfmpn  30556  ballotlem1ri  30596  sgnmulsgn  30611  plymul02  30623  signsplypnf  30627  signsply0  30628  signswrid  30635  prodfzo03  30681  itgexpif  30684  circlemethhgt  30721  hgt750lemb  30734  indispconn  31216  connpconn  31217  iccllysconn  31232  cvmopnlem  31260  cvmliftlem15  31280  cvmlift2lem3  31287  mrsubff  31409  mrsubccat  31415  circum  31568  noextend  31819  nosupbnd2lem1  31861  elhf2  32282  topdifinfindis  33194  icoreelrn  33209  finxpreclem2  33227  finixpnum  33394  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem5  33414  poimirlem10  33419  poimirlem22  33431  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  dvtan  33460  itg2addnclem  33461  ftc1anclem5  33489  dvasin  33496  dvreasin  33498  dvreacos  33499  areacirclem1  33500  areacirc  33505  bnd2lem  33590  prdsbnd  33592  cntotbnd  33595  cnpwstotbnd  33596  isdrngo2  33757  prter2  34166  eqlkr2  34387  tendoidcl  36057  cdlemk56  36259  dihpN  36625  mapdhval  37013  hlhillcs  37250  isnacs3  37273  diophrw  37322  lzenom  37333  diophin  37336  pellexlem5  37397  pw2f1ocnv  37604  dnnumch2  37615  kelac2lem  37634  kelac2  37635  dfac21  37636  pwfi2f1o  37666  frlmpwfi  37668  mpaaeu  37720  rngunsnply  37743  mendbas  37754  mendplusgfval  37755  mendmulrfval  37757  mendsca  37759  mendvscafval  37760  subrgacs  37770  sdrgacs  37771  cntzsdrg  37772  idomodle  37774  proot1ex  37779  deg1mhm  37785  itgpowd  37800  trclubgNEW  37925  dmtrcl  37934  rntrcl  37935  brfvidRP  37980  trclrelexplem  38003  relexp01min  38005  trclimalb2  38018  dssmapfvd  38311  ntrk0kbimka  38337  ntrrn  38420  dssmapntrcls  38426  amgm2d  38501  amgm3d  38502  amgm4d  38503  hashnzfzclim  38521  ofsubid  38523  ofdivrec  38525  dvconstbi  38533  fzisoeu  39514  iuneqfzuzlem  39550  sumnnodd  39862  liminfgf  39990  negcncfg  40094  cnfdmsn  40095  dvmptresicc  40134  itgcoscmulx  40185  stoweidlem13  40230  stoweidlem26  40243  stoweidlem34  40251  stoweidlem42  40259  stoweidlem44  40261  stoweidlem48  40265  stoweidlem62  40279  stoweid  40280  stirlinglem7  40297  stirlinglem11  40301  stirlinglem12  40302  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem24  40348  fourierdlem48  40371  fourierdlem49  40372  fourierdlem62  40385  fourierdlem70  40393  fourierdlem80  40403  fourierdlem83  40406  fourierdlem85  40408  fourierdlem102  40425  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem114  40437  etransclem18  40469  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem35  40486  etransclem46  40497  ovolval5lem3  40868  setsidel  41346  iccpartipre  41357  iccpartiltu  41358  fmtnoprmfac2lem1  41478  mod42tp1mod8  41519  sfprmdvdsmersenne  41520  perfectALTVlem2  41631  stgoldbwt  41664  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem2  41694  upwlksfval  41716  sprval  41729  sprbisymrel  41749  uspgrbisymrelALT  41763  idmgmhm  41788  mgmplusgiopALT  41830  sgrp2sgrp  41864  isrnghm  41892  lidlmmgm  41925  2zrngnmlid  41949  dfrngc2  41972  rnghmsscmap2  41973  rnghmsscmap  41974  rngchomfvalALTV  41984  rngcidALTV  41991  funcrngcsetcALT  41999  dfringc2  42018  rhmsscmap2  42019  rhmsscmap  42020  rhmsscrnghm  42026  rngcresringcat  42030  funcringcsetcALTV2lem8  42043  ringchomfvalALTV  42047  ringcidALTV  42054  funcringcsetclem8ALTV  42066  srhmsubc  42076  fldc  42083  rngcrescrhm  42085  rhmsubclem3  42088  srhmsubcALTV  42094  fldcALTV  42101  rngcrescrhmALTV  42103  altgsumbcALT  42131  zlmodzxzel  42133  zlmodzxzsubm  42137  zlmodzxzsub  42138  gsumpr  42139  scmsuppss  42153  ply1mulgsum  42178  dmatALTbas  42190  lcoop  42200  lincval0  42204  lco0  42216  linds0  42254  snlindsntorlem  42259  lmod1lem2  42277  lmod1lem3  42278  lmod1zr  42282  lmod1zrnlvec  42283  zlmodzxznm  42286  zlmodzxzldeplem4  42292  expnegico01  42308  pw2m1lepw2m1  42310  fldivexpfllog2  42359  blennnelnn  42370  blenpw2  42372  nnpw2pmod  42377  blennnt2  42383  nnolog2flm1  42384  digfval  42391  dignnld  42397  dig2nn0ld  42398  0dig2nn0e  42406  0dig2nn0o  42407  amgmwlem  42548  amgmlemALT  42549  amgmw2d  42550