MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp1i Structured version   Unicode version

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
StepHypRef Expression
1 mp1i.1 . . 3  |-  ph
2 mp1i.2 . . 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  5244  relcoi2  5383  fvrnressn  6094  isomin  6243  isoini  6244  supp0  6930  suppval1  6931  suppssr  6957  dmtpos  6993  mpt2curryd  7024  oaabs2  7354  mapsncnv  7526  boxcutc  7573  domunsncan  7678  pw2f1o  7683  unxpdom2  7786  sucxpdom  7787  findcard2d  7819  ac6sfi  7821  xpfi  7848  imafi  7873  snopfsupp  7912  fifo  7952  ordtypelem4  8036  oismo  8055  wofib  8060  brwdom2  8088  canthwdom  8094  cantnfval  8172  cantnflt  8176  cantnff  8178  cantnf0  8179  cantnfp1lem1  8182  cantnfp1lem3  8184  cantnflem1b  8190  cantnflem1  8193  cnfcom  8204  cnfcom2lem  8205  ranksnb  8297  tskwe  8383  cardidm  8392  infxpenc  8447  fseqdom  8455  dfac8clem  8461  dfac12lem2  8572  infmap2  8646  isfin4-3  8743  fin23lem14  8761  fin23lem40  8779  isf34lem7  8807  isf34lem6  8808  fin1a2lem12  8839  hsmexlem4  8857  hsmexlem5  8858  ac5b  8906  alephexp1  9002  alephsuc3  9003  fpwwe2lem8  9061  fpwwe2lem13  9066  canthwe  9075  canthp1lem2  9077  gchcda1  9080  pwfseqlem5  9087  wunco  9157  prlem934  9457  supsrlem  9534  msqge0  10134  negfi  10554  ofnegsub  10607  ofsubge0  10608  xaddpnf1  11519  supxrmnf  11603  injresinjlem  12021  uzindi  12191  seqfeq4  12259  seqof  12267  bcval5  12500  hashdomi  12556  hash1snb  12588  brfi1uzind  12641  ccatlen  12708  lswccatn0lsw  12721  eqs1  12735  s111  12737  swrd0  12775  swrdspsleq  12790  wrdeqs1cat  12816  reps  12858  repsw0  12865  repswccat  12873  repswrevw  12874  lswcshw  12899  cshwsexa  12908  scshwfzeqfzo  12910  wrdlen2i  13000  relexpsucnnr  13067  relexpaddg  13095  shftfib  13114  limsupcl  13507  limsupclOLD  13508  limsupgf  13511  limsupval2  13518  limsupval2OLD  13519  isercolllem3  13708  modfsummods  13831  ackbijnn  13864  supcvg  13892  fprodfac  14005  fallfac0  14059  bpoly4  14090  ege2le3  14122  rpnnen2lem5  14249  ruclem11  14270  fsumdvds  14326  bitsinv2  14391  sadaddlem  14414  smupf  14426  smup0  14427  smu01lem  14433  3lcm2e6woprm  14545  6lcm4e12  14546  lcmslefacOLD  14551  lcmfunsnlem1  14572  lcmfunsnlem2lem1  14573  lcmfunsnlem2  14575  isprm6  14628  coprmprod  14640  hashdvds  14683  reumodprminv  14709  prmreclem6  14819  vdwlem13  14897  ramtlecl  14905  0ram  14932  prmdvdsprmo  14954  fvprmselgcd1  14957  prmgaplcmlem1  14963  prmgaplcmlem1OLD  14966  prmdvdsprmorOLD  14969  prmgaplem7  14981  prmgaplcm  14985  cshwshashnsame  15028  prmlem0  15031  wunndx  15091  prdsval  15303  xpsbas  15422  xpsadd  15424  xpsmul  15425  xpssca  15426  xpsvsca  15427  xpsless  15428  xpsle  15429  mreexexlem2d  15493  mreacs  15506  acsfn  15507  isofn  15622  ciclcl  15649  cicrcl  15650  cicsym  15651  cicer  15653  idfu2nd  15724  idfucl  15728  fucsect  15819  initoeu2lem1  15851  initoeu2lem2  15852  setccatid  15921  setcepi  15925  catchomfval  15935  estrccatid  15959  estrreslem1  15964  estrreslem2  15965  estrres  15966  funcestrcsetclem8  15974  fullestrcsetc  15978  embedsetcestrclem  15984  funcsetcestrclem8  15989  uncfval  16061  oduglb  16327  odumeet  16328  odulub  16329  odujoin  16330  isipodrs  16349  fpwipodrs  16352  isacs4lem  16356  isacs5lem  16357  idmhm  16533  submacs  16554  frmdup1  16590  mgmnsgrpex  16607  mulgneg2  16727  subgacs  16794  nsgacs  16795  idrespermg  16994  psgnunilem5  17077  psgnsn  17103  odf1o2  17151  frgpuplem  17348  cygctb  17452  gsumzunsnd  17514  gsum2dlem2  17529  gsummptnn0fz  17541  dprdsubg  17583  dmdprdsplit2lem  17604  dmdprdpr  17608  dprdpr  17609  dpjeq  17618  ablfac1eulem  17631  pgpfac1lem2  17634  pgpfaclem1  17640  srgbinomlem4  17702  unitgrp  17821  isirred  17853  brric  17898  mptscmfsupp0  18079  lssacs  18116  pwssplit1  18208  lbsextlem2  18308  lbsextlem3  18309  isnzr2hash  18414  0ring01eqbi  18423  rng1nnzr  18424  psrass1lem  18527  psrlidm  18553  resspsradd  18566  resspsrmul  18567  resspsrvsca  18568  mplcoe5lem  18617  ltbwe  18622  coe1fsupp  18733  psropprmul  18757  coe1add  18783  coe1mul2lem1  18786  coe1tm  18792  cply1coe0bi  18820  evls1rhmlem  18836  evl1sca  18848  evl1var  18850  pf1mpf  18866  pf1ind  18869  xrsmcmn  18917  xrs1mnd  18932  xrs10  18933  gsumfsum  18960  zringlpir  18981  zringcyg  18982  zndvds  19042  regsumsupp  19112  uvcvv1  19269  lsslinds  19311  matmulr  19385  ofco2  19398  mat0dimbas0  19413  mat1dimelbas  19418  mat1f1o  19425  dmatval  19439  scmatghm  19480  mavmul0  19499  mavmul0g  19500  m1detdiag  19544  mdetunilem9  19567  maducoeval2  19587  madugsum  19590  smadiadetlem0  19608  smadiadetlem1a  19610  smadiadetlem4  19616  smadiadetglem1  19618  smadiadetglem2  19619  smadiadetg  19620  cramer0  19637  cpmat  19655  mat2pmatfval  19669  cpm2mfval  19695  m2cpminvid2lem  19700  pmatcollpw3fi1lem2  19733  pmatcollpw3fi1  19734  idpm2idmp  19747  pm2mpmhmlem2  19765  chpmatfval  19776  chfacfscmulfsupp  19805  chfacfpmmulfsupp  19809  cpmidpmatlem2  19817  cpmadugsumlemF  19822  cpmidgsum2  19825  cpmadumatpolylem1  19827  cayhamlem3  19833  cayhamlem4  19834  indistopon  19938  mreclatdemoBAD  20034  mnfnei  20159  resthauslem  20301  sshauslem  20310  discmp  20335  conima  20362  1stcfb  20382  hauseqlcld  20583  xkoptsub  20591  xkofvcn  20621  idqtop  20643  tgqtop  20649  kqdisj  20669  xpstopnlem1  20746  xpstopnlem2  20748  ufildom1  20863  alexsubb  20983  alexsubALTlem3  20986  ptcmplem2  20990  ptcmplem3  20991  tmdgsum  21032  ustneism  21160  ustuqtop1  21178  iducn  21220  prdsmet  21307  imasdsf1olem  21310  xpsxmet  21317  xpsdsval  21318  xpsmet  21319  prdsbl  21428  met1stc  21458  prdsxmslem2  21466  xpsxms  21471  xpsms  21472  psmetutop  21504  dscmet  21509  nmoffn  21634  nmofval  21637  nmolb  21640  nmof  21642  cnbl0  21696  xrsmopn  21732  xrge0gsumle  21753  xrge0tsms  21754  negfcncf  21838  cnrehmeo  21868  lebnum  21879  xlebnum  21880  reparphti  21912  pcopt  21937  pcopt2  21938  pcorevcl  21940  pcorevlem  21941  pi1xfrval  21969  pi1xfrcnvlem  21971  pi1xfrcnv  21972  pi1cof  21974  pi1coval  21975  nmhmcn  22018  cphsubrglem  22039  csscld  22104  cmetcaulem  22142  cmpcmet  22171  ovolunlem1  22319  ovolicc2lem4  22342  ioovolcl  22390  ioorcl2  22392  uniioovol  22404  uniioombllem4  22412  uniioombllem5  22413  uniioombllem6  22414  dyadmbllem  22425  mbfsub  22486  itg1climres  22540  xrge0f  22557  itg2ge0  22561  itg2i1fseq2  22582  ibl0  22612  ellimc2  22700  limcflf  22704  dvreslem  22732  dvidlem  22738  dvid  22740  cpnres  22759  dvaddbr  22760  dvmulbr  22761  dvfre  22773  dvexp  22775  dvrec  22777  dvmptid  22779  dvmptc  22780  dvmptntr  22793  dvexp3  22798  dvlipcn  22814  dveq0  22820  dv11cn  22821  lhop2  22835  ftc1a  22857  tdeglem1  22875  tdeglem3  22876  tdeglem4  22877  tdeglem2  22878  mdeg0  22887  mdegle0  22894  ply1remlem  22979  fta1glem2  22983  plypf1  23025  coe0  23069  dvply1  23096  elqaalem3  23133  aaliou2b  23153  aaliou3lem8  23157  aaliou3lem7  23161  taylfvallem  23169  taylf  23172  tayl0  23173  taylpfval  23176  taylply  23180  dvtaylp  23181  taylthlem1  23184  taylthlem2  23185  ulmdvlem1  23211  ulmdvlem2  23212  ulmdvlem3  23213  radcnvcl  23228  psercnlem2  23235  psercn  23237  pserdv  23240  abelthlem3  23244  abelth  23252  sincn  23255  coscn  23256  reefgim  23261  tangtx  23316  pige3  23328  cosordlem  23336  logcn  23448  dvlog  23452  advlog  23455  advlogexp  23456  logtayl  23461  logccv  23464  dvcxp1  23536  dvcncxp1  23539  cxpcn3lem  23543  cxpcn3  23544  resqrtcn  23545  sqrtcn  23546  loglesqrt  23554  logbfval  23583  logblog  23585  isosctrlem2  23604  dquartlem1  23633  quart  23643  atancj  23692  efiatan  23694  atantan  23705  atanbndlem  23707  atansopn  23714  dvatan  23717  atantayl  23719  leibpilem2  23723  leibpi  23724  log2tlbnd  23727  rlimcnp2  23748  efrlim  23751  divsqrtsumlem  23761  jensenlem1  23768  jensenlem2  23769  jensen  23770  amgmlem  23771  amgm  23772  emcllem4  23780  emcllem7  23783  lgamcvg2  23836  gamcvg2lem  23840  wilthlem2  23850  wilthlem3  23851  basellem6  23866  chtrpcl  23956  ppiltx  23958  1sgm2ppw  23982  chtlepsi  23988  chpub  24002  logfacbnd3  24005  logfacrlim  24006  perfectlem2  24012  dchrelbas2  24019  dchrabs  24042  dchrhash  24053  bposlem7  24072  lgsdir2lem5  24109  lgsqrlem1  24123  lgseisenlem4  24134  lgsquad2lem1  24140  lgsquad3  24143  chpo1ub  24172  vmadivsumb  24175  rpvmasumlem  24179  dchrisumlem2  24182  dchrmusumlema  24185  dchrvmasumlem2  24190  dchrvmasumlema  24192  dchrvmasumiflem1  24193  dchrisum0flblem1  24200  dchrisum0lem1  24208  rplogsum  24219  mudivsum  24222  logdivsum  24225  mulog2sumlem2  24227  vmalogdivsum2  24230  2vmadivsumlem  24232  log2sumbnd  24236  selberglem2  24238  selbergb  24241  selberg2lem  24242  selberg2b  24244  selberg3lem1  24249  selberg4lem1  24252  selberg4  24253  pntrsumo1  24257  pntrlog2bndlem2  24270  pntrlog2bndlem3  24271  pntrlog2bndlem4  24272  pntrlog2bndlem5  24273  pntibndlem1  24281  pntibndlem2  24283  pntibndlem3  24284  pntlemb  24289  pntlemr  24294  pntlemf  24297  pntlem3  24301  pnt  24306  qabvle  24317  padicabv  24322  ostth1  24325  istrkg2ld  24362  tgldimor  24400  motgrp  24439  perpln1  24603  perpln2  24604  isperp  24605  uhgrares  24872  umgrares  24888  edgopval  24904  usgrares  24933  nbgraop  24987  nbgraopALT  24988  nbgraf1o0  25010  cusgra0v  25024  cusgra1v  25025  cusgraexilem2  25031  sizeusglecusg  25050  isuvtx  25052  2trllemH  25118  wlkntrllem3  25127  2wlklem1  25163  usgra2wlkspthlem1  25183  usgra2wlkspthlem2  25184  constr3trllem3  25216  constr3pthlem3  25221  wwlkn  25246  wlkiswwlk2  25261  wwlkn0s  25269  usg2wlkeq  25272  wwlkexthasheq  25298  wlknwwlknvbij  25304  clwwlkn  25331  clwwlkn2  25339  clwlkisclwwlklem2  25350  clwwlkvbij  25365  eclclwwlkn0  25395  hashecclwwlkn1  25398  usghashecclwwlk  25399  vdgr0  25464  rusgrasn  25509  eupatrl  25532  eupares  25539  vdegp1ai  25548  vdegp1bi  25549  frgra3v  25566  frgrancvvdeqlem9  25605  frgrancvvdgeq  25607  frg2wot1  25621  usgreghash2spotv  25630  extwwlkfablem2  25642  numclwwlkovf2  25648  numclwwlk2lem3  25670  vsfval  26090  ipasslem7  26313  minvecolem2  26353  h2hcau  26458  h2hlm  26459  hlimadd  26672  hhsscms  26756  chocunii  26780  occllem  26782  leopnmid  27617  opsqrlem1  27619  hmopidmchi  27630  mdslj1i  27798  addltmulALT  27925  imadifxp  28042  xaddeq0  28164  xrge0npcan  28286  gsumle  28371  xrge0tsmsd  28378  locfinreflem  28497  locfinref  28498  xpinpreima2  28543  cnre2csqlem  28546  tpr2rico  28548  ordtrestNEW  28557  ordtrest2NEW  28559  mndpluscn  28562  pnfneige0  28587  qqhghm  28622  qqhrhm  28623  qqhcn  28625  qqhucn  28626  rrhcn  28631  rrhre  28655  esumsplit  28704  esumpr  28717  esumfsup  28721  sigaclcu2  28772  pwsiga  28782  prsiga  28783  sigapildsys  28814  measvuni  28866  elmbfmvol2  28919  mbfmcnt  28920  sxbrsigalem1  28937  sxbrsiga  28942  omsfval  28946  carsgclctunlem2  28971  sibf0  28986  sitgclg  28994  sitmval  29001  eulerpartgbij  29022  eulerpartlemgh  29028  isrrvv  29093  rrvadd  29102  rrvmulc  29103  dstrvprob  29121  coinflipspace  29130  coinfliprv  29132  ballotlemfmpn  29144  ballotlem1ri  29184  sgnmulsgn  29199  plymul02  29214  signsplypnf  29218  signsply0  29219  signswrid  29226  indispcon  29736  conpcon  29737  iccllyscon  29752  cvmopnlem  29780  cvmliftlem15  29800  cvmlift2lem3  29807  mrsubff  29929  mrsubccat  29935  circum  30097  elhf2  30718  topdifinfindis  31474  icoreelrn  31489  finixpnum  31624  poimirlem5  31639  poimirlem10  31644  poimirlem22  31656  poimirlem25  31659  poimirlem26  31660  poimirlem27  31661  poimirlem28  31662  poimirlem29  31663  poimirlem31  31665  poimirlem32  31666  mblfinlem3  31673  mblfinlem4  31674  ismblfin  31675  ovoliunnfl  31676  voliunnfl  31678  volsupnfl  31679  dvtan  31686  itg2addnclem  31687  ftc1anclem5  31715  dvasin  31722  dvreasin  31724  dvreacos  31725  areacirclem1  31726  areacirc  31731  bnd2lem  31817  prdsbnd  31819  cntotbnd  31822  cnpwstotbnd  31823  isdrngo2  31891  prter2  32151  eqlkr2  32365  tendoidcl  34035  cdlemk56  34237  dihpN  34603  mapdhval  34991  hlhillcs  35228  isnacs3  35251  diophrw  35300  lzenom  35311  diophin  35314  pellexlem5  35377  pw2f1ocnv  35588  dnnumch2  35599  kelac2lem  35618  kelac2  35619  dfac21  35620  pwfi2f1o  35650  frlmpwfi  35652  mpaaeu  35705  rngunsnply  35728  mendbas  35739  mendplusgfval  35740  mendmulrfval  35742  mendsca  35744  mendvscafval  35745  subrgacs  35755  sdrgacs  35756  cntzsdrg  35757  idomodle  35759  phisum  35765  proot1ex  35767  deg1mhm  35773  itgpowd  35788  brfvidRP  35909  trclrelexplem  35932  relexp01min  35934  trclimalb2  35947  amgm2d  36277  amgm3d  36278  amgm4d  36279  hashnzfzclim  36298  ofsubid  36300  ofdivrec  36302  dvconstbi  36310  fzisoeu  37117  iuneqfzuzlem  37156  sumnnodd  37272  negcncfg  37320  cnfdmsn  37321  divcncf  37323  dvmptresicc  37353  itgcoscmulx  37405  stoweidlem13  37432  stoweidlem26  37445  stoweidlem34  37454  stoweidlem42  37462  stoweidlem44  37464  stoweidlem48  37468  stoweidlem62  37482  stoweidlem62OLD  37483  stoweid  37484  stirlinglem7  37501  stirlinglem11  37505  stirlinglem12  37506  dirkeritg  37523  dirkercncflem2  37525  dirkercncflem4  37527  fourierdlem16  37544  fourierdlem21  37549  fourierdlem22  37550  fourierdlem24  37552  fourierdlem48  37576  fourierdlem49  37577  fourierdlem62  37590  fourierdlem70  37598  fourierdlem80  37608  fourierdlem83  37611  fourierdlem85  37613  fourierdlem102  37630  fourierdlem104  37632  fourierdlem111  37639  fourierdlem112  37640  fourierdlem114  37642  etransclem18  37674  etransclem23  37679  etransclem24  37680  etransclem25  37681  etransclem35  37691  etransclem46  37702  mod2eq1n2dvds  38105  iccpartipre  38115  iccpartiltu  38116  perfectALTVlem2  38224  stgoldbwt  38257  nnsum3primesgbe  38267  nnsum4primesodd  38271  nnsum4primesoddALTV  38272  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  bgoldbtbndlem2  38281  uhgrepe  38438  uhgres  38439  gordopval  38450  gsizopval  38451  usgedgnlp  38470  isfusgracl  38486  isfusgraclALT  38488  usgo0s0  38495  usgo0s0ALT  38496  usgo1s0ALT  38497  usgo1s0  38502  usgresvm1  38503  usgfis  38506  usgresvm1ALT  38507  usgrafiedgALT  38511  idmgmhm  38536  mgmplusgiopALT  38578  sgrp2sgrp  38612  isrnghm  38640  lidlmmgm  38673  2zrngnmlid  38697  dfrngc2  38722  rnghmsscmap2  38723  rnghmsscmap  38724  rngchomfvalALTV  38734  rngcidALTV  38741  funcrngcsetcALT  38749  dfringc2  38768  rhmsscmap2  38769  rhmsscmap  38770  rhmsscrnghm  38776  rngcresringcat  38780  funcringcsetcALTV2lem8  38793  ringchomfvalALTV  38797  ringcidALTV  38804  funcringcsetclem8ALTV  38816  srhmsubc  38826  fldc  38833  rngcrescrhm  38835  rhmsubclem3  38838  srhmsubcALTV  38845  fldcALTV  38852  rngcrescrhmALTV  38854  altgsumbcALT  38884  zlmodzxzel  38886  zlmodzxzsubm  38890  zlmodzxzsub  38891  gsumpr  38892  scmsuppss  38907  ply1mulgsum  38932  dmatALTbas  38944  lcoop  38954  lincval0  38958  lco0  38970  linds0  39008  snlindsntorlem  39013  lmod1lem2  39031  lmod1lem3  39032  lmod1zr  39036  lmod1zrnlvec  39037  zlmodzxznm  39040  zlmodzxzldeplem4  39046  expnegico01  39065  pw2m1lepw2m1  39069  fldivexpfllog2  39127  blennnelnn  39138  blenpw2  39140  nnpw2pmod  39145  blennnt2  39151  nnolog2flm1  39152  digfval  39159  dignnld  39165  dig2nn0ld  39166  0dig2nn0e  39174  0dig2nn0o  39175
  Copyright terms: Public domain W3C validator