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  5181  relcoi2  5320  fvrnressn  6033  isomin  6182  isoini  6183  supp0  6869  suppval1  6870  suppssr  6896  dmtpos  6935  mpt2curryd  6966  oaabs2  7296  mapsncnv  7468  boxcutc  7515  domunsncan  7620  pw2f1o  7625  unxpdom2  7728  sucxpdom  7729  findcard2d  7761  ac6sfi  7763  xpfi  7790  imafi  7815  snopfsupp  7854  fifo  7894  ordtypelem4  7984  oismo  8003  wofib  8008  brwdom2  8036  canthwdom  8042  cantnfval  8120  cantnflt  8124  cantnff  8126  cantnf0  8127  cantnfp1lem1  8130  cantnfp1lem3  8132  cantnflem1b  8138  cantnflem1  8141  cnfcom  8152  cnfcom2lem  8153  ranksnb  8245  tskwe  8331  cardidm  8340  infxpenc  8395  fseqdom  8403  dfac8clem  8409  dfac12lem2  8520  infmap2  8594  isfin4-3  8691  fin23lem14  8709  fin23lem40  8727  isf34lem7  8755  isf34lem6  8756  fin1a2lem12  8787  hsmexlem4  8805  hsmexlem5  8806  ac5b  8854  alephexp1  8950  alephsuc3  8951  fpwwe2lem8  9008  fpwwe2lem13  9013  canthwe  9022  canthp1lem2  9024  gchcda1  9027  pwfseqlem5  9034  wunco  9104  prlem934  9404  supsrlem  9481  msqge0  10081  negfi  10500  ofnegsub  10553  ofsubge0  10554  xaddpnf1  11465  supxrmnf  11549  injresinjlem  11969  uzindi  12139  seqfeq4  12207  seqof  12215  bcval5  12448  hashdomi  12504  hash1snb  12536  hashge2el2difr  12581  fi1uzind  12593  ccatlen  12664  lswccatn0lsw  12677  eqs1  12691  s111  12693  swrd0  12731  swrdspsleq  12746  wrdeqs1cat  12772  reps  12814  repsw0  12821  repswccat  12829  repswrevw  12830  lswcshw  12855  cshwsexa  12864  scshwfzeqfzo  12866  wrdlen2i  12960  relexpsucnnr  13027  relexpaddg  13055  shftfib  13074  limsupcl  13467  limsupclOLD  13468  limsupgf  13471  limsupval2  13478  limsupval2OLD  13479  isercolllem3  13668  modfsummods  13791  ackbijnn  13824  supcvg  13852  fprodfac  13965  fallfac0  14019  bpoly4  14050  ege2le3  14082  rpnnen2lem5  14209  ruclem11  14230  fsumdvds  14286  bitsinv2  14355  sadaddlem  14378  smupf  14390  smup0  14391  smu01lem  14397  3lcm2e6woprm  14518  6lcm4e12  14519  lcmslefacOLD  14524  lcmfunsnlem1  14548  lcmfunsnlem2lem1  14549  lcmfunsnlem2  14551  isprm6  14604  coprmprod  14616  hashdvds  14661  reumodprminv  14693  prmreclem6  14803  vdwlem13  14881  ramtlecl  14889  0ram  14916  prmdvdsprmo  14938  fvprmselgcd1  14941  prmgaplcmlem1  14947  prmgaplcmlem1OLD  14950  prmdvdsprmorOLD  14953  prmgaplem7  14965  prmgaplcm  14969  cshwshashnsame  15012  prmlem0  15015  wunndx  15075  prdsval  15291  xpsbas  15418  xpsadd  15420  xpsmul  15421  xpssca  15422  xpsvsca  15423  xpsless  15424  xpsle  15425  mreexexlem2d  15489  mreacs  15502  acsfn  15503  isofn  15618  ciclcl  15645  cicrcl  15646  cicsym  15647  cicer  15649  idfu2nd  15720  idfucl  15724  fucsect  15815  initoeu2lem1  15847  initoeu2lem2  15848  setccatid  15917  setcepi  15921  catchomfval  15931  estrccatid  15955  estrreslem1  15960  estrreslem2  15961  estrres  15962  funcestrcsetclem8  15970  fullestrcsetc  15974  embedsetcestrclem  15980  funcsetcestrclem8  15985  uncfval  16057  oduglb  16323  odumeet  16324  odulub  16325  odujoin  16326  isipodrs  16345  fpwipodrs  16348  isacs4lem  16352  isacs5lem  16353  idmhm  16529  submacs  16550  frmdup1  16586  mgmnsgrpex  16603  mulgneg2  16723  subgacs  16790  nsgacs  16791  idrespermg  16990  psgnunilem5  17073  psgnsn  17099  odf1o2  17160  frgpuplem  17360  cygctb  17464  gsumzunsnd  17526  gsum2dlem2  17541  gsummptnn0fz  17553  dprdsubg  17595  dmdprdsplit2lem  17616  dmdprdpr  17620  dprdpr  17621  dpjeq  17630  ablfac1eulem  17643  pgpfac1lem2  17646  pgpfaclem1  17652  srgbinomlem4  17714  unitgrp  17833  isirred  17865  brric  17910  mptscmfsupp0  18091  lssacs  18128  pwssplit1  18220  lbsextlem2  18320  lbsextlem3  18321  isnzr2hash  18426  0ring01eqbi  18435  rng1nnzr  18436  psrass1lem  18539  psrlidm  18565  resspsradd  18578  resspsrmul  18579  resspsrvsca  18580  mplcoe5lem  18629  ltbwe  18634  coe1fsupp  18745  psropprmul  18769  coe1add  18795  coe1mul2lem1  18798  coe1tm  18804  cply1coe0bi  18832  evls1rhmlem  18848  evl1sca  18860  evl1var  18862  pf1mpf  18878  pf1ind  18881  xrsmcmn  18929  xrs1mnd  18944  xrs10  18945  gsumfsum  18972  zringlpir  18995  zringlpirOLD  18996  zringcyg  18997  zndvds  19057  regsumsupp  19127  uvcvv1  19284  lsslinds  19326  matmulr  19400  ofco2  19413  mat0dimbas0  19428  mat1dimelbas  19433  mat1f1o  19440  dmatval  19454  scmatghm  19495  mavmul0  19514  mavmul0g  19515  m1detdiag  19559  mdetunilem9  19582  maducoeval2  19602  madugsum  19605  smadiadetlem0  19623  smadiadetlem1a  19625  smadiadetlem4  19631  smadiadetglem1  19633  smadiadetglem2  19634  smadiadetg  19635  cramer0  19652  cpmat  19670  mat2pmatfval  19684  cpm2mfval  19710  m2cpminvid2lem  19715  pmatcollpw3fi1lem2  19748  pmatcollpw3fi1  19749  idpm2idmp  19762  pm2mpmhmlem2  19780  chpmatfval  19791  chfacfscmulfsupp  19820  chfacfpmmulfsupp  19824  cpmidpmatlem2  19832  cpmadugsumlemF  19837  cpmidgsum2  19840  cpmadumatpolylem1  19842  cayhamlem3  19848  cayhamlem4  19849  indistopon  19953  mreclatdemoBAD  20049  mnfnei  20174  resthauslem  20316  sshauslem  20325  discmp  20350  conima  20377  1stcfb  20397  hauseqlcld  20598  xkoptsub  20606  xkofvcn  20636  idqtop  20658  tgqtop  20664  kqdisj  20684  xpstopnlem1  20761  xpstopnlem2  20763  ufildom1  20878  alexsubb  20998  alexsubALTlem3  21001  ptcmplem2  21005  ptcmplem3  21006  tmdgsum  21047  ustneism  21175  ustuqtop1  21193  iducn  21235  prdsmet  21322  imasdsf1olem  21325  xpsxmet  21332  xpsdsval  21333  xpsmet  21334  prdsbl  21443  met1stc  21473  prdsxmslem2  21481  xpsxms  21486  xpsms  21487  psmetutop  21519  dscmet  21524  nmoffn  21653  nmofval  21656  nmolb  21659  nmof  21661  nmoffnOLD  21674  nmofvalOLD  21675  nmolbOLD  21678  nmofOLD  21679  cnbl0  21731  xrsmopn  21767  xrge0gsumle  21788  xrge0tsms  21789  negfcncf  21888  cnrehmeo  21918  lebnum  21932  xlebnum  21933  reparphti  21965  pcopt  21990  pcopt2  21991  pcorevcl  21993  pcorevlem  21994  pi1xfrval  22022  pi1xfrcnvlem  22024  pi1xfrcnv  22025  pi1cof  22027  pi1coval  22028  nmhmcn  22071  cphsubrglem  22092  csscld  22157  cmetcaulem  22195  cmpcmet  22224  ovolunlem1  22387  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  ioovolcl  22459  ioorcl2  22461  uniioovol  22473  uniioombllem4  22481  uniioombllem5  22482  uniioombllem6  22483  dyadmbllem  22494  mbfsub  22555  itg1climres  22609  xrge0f  22626  itg2ge0  22630  itg2i1fseq2  22651  ibl0  22681  ellimc2  22769  limcflf  22773  dvreslem  22801  dvidlem  22807  dvid  22809  cpnres  22828  dvaddbr  22829  dvmulbr  22830  dvfre  22842  dvexp  22844  dvrec  22846  dvmptid  22848  dvmptc  22849  dvmptntr  22862  dvexp3  22867  dvlipcn  22883  dveq0  22889  dv11cn  22890  lhop2  22904  ftc1a  22926  tdeglem1  22944  tdeglem3  22945  tdeglem4  22946  tdeglem2  22947  mdeg0  22956  mdegle0  22963  ply1remlem  23050  fta1glem2  23054  plypf1  23103  coe0  23147  dvply1  23174  elqaalem3  23211  elqaalem3OLD  23214  aaliou2b  23234  aaliou3lem8  23238  aaliou3lem7  23242  taylfvallem  23250  taylf  23253  tayl0  23254  taylpfval  23257  taylply  23261  dvtaylp  23262  taylthlem1  23265  taylthlem2  23266  ulmdvlem1  23292  ulmdvlem2  23293  ulmdvlem3  23294  radcnvcl  23309  psercnlem2  23316  psercn  23318  pserdv  23321  abelthlem3  23325  abelth  23333  sincn  23336  coscn  23337  reefgim  23342  tangtx  23397  pige3  23409  cosordlem  23417  logcn  23529  dvlog  23533  advlog  23536  advlogexp  23537  logtayl  23542  logccv  23545  dvcxp1  23617  dvcncxp1  23620  cxpcn3lem  23624  cxpcn3  23625  resqrtcn  23626  sqrtcn  23627  loglesqrt  23635  logbfval  23664  logblog  23666  isosctrlem2  23685  dquartlem1  23714  quart  23724  atancj  23773  efiatan  23775  atantan  23786  atanbndlem  23788  atansopn  23795  dvatan  23798  atantayl  23800  leibpilem2  23804  leibpi  23805  log2tlbnd  23808  rlimcnp2  23829  efrlim  23832  divsqrtsumlem  23842  jensenlem1  23849  jensenlem2  23850  jensen  23851  amgmlem  23852  amgm  23853  emcllem4  23861  emcllem7  23864  lgamcvg2  23917  gamcvg2lem  23921  wilthlem2  23931  wilthlem3  23932  basellem6  23949  chtrpcl  24039  ppiltx  24041  1sgm2ppw  24065  chtlepsi  24071  chpub  24085  logfacbnd3  24088  logfacrlim  24089  perfectlem2  24095  dchrelbas2  24102  dchrabs  24125  dchrhash  24136  bposlem7  24155  lgsdir2lem5  24192  lgsqrlem1  24206  lgseisenlem4  24217  lgsquad2lem1  24223  lgsquad3  24226  chpo1ub  24255  vmadivsumb  24258  rpvmasumlem  24262  dchrisumlem2  24265  dchrmusumlema  24268  dchrvmasumlem2  24273  dchrvmasumlema  24275  dchrvmasumiflem1  24276  dchrisum0flblem1  24283  dchrisum0lem1  24291  rplogsum  24302  mudivsum  24305  logdivsum  24308  mulog2sumlem2  24310  vmalogdivsum2  24313  2vmadivsumlem  24315  log2sumbnd  24319  selberglem2  24321  selbergb  24324  selberg2lem  24325  selberg2b  24327  selberg3lem1  24332  selberg4lem1  24335  selberg4  24336  pntrsumo1  24340  pntrlog2bndlem2  24353  pntrlog2bndlem3  24354  pntrlog2bndlem4  24355  pntrlog2bndlem5  24356  pntibndlem1  24364  pntibndlem2  24366  pntibndlem3  24367  pntlemb  24372  pntlemr  24377  pntlemf  24380  pntlem3  24384  pnt  24389  qabvle  24400  padicabv  24405  ostth1  24408  istrkg2ld  24445  tgldimor  24483  tgcgr4  24513  motgrp  24525  perpln1  24692  perpln2  24693  isperp  24694  uhgrares  24972  umgrares  24988  edgopval  25004  usgrares  25033  nbgraop  25088  nbgraopALT  25089  nbgraf1o0  25111  cusgra0v  25125  cusgra1v  25126  cusgraexilem2  25132  sizeusglecusg  25151  isuvtx  25153  2trllemH  25219  wlkntrllem3  25228  2wlklem1  25264  usgra2wlkspthlem1  25284  usgra2wlkspthlem2  25285  constr3trllem3  25317  constr3pthlem3  25322  wwlkn  25347  wlkiswwlk2  25362  wwlkn0s  25370  usg2wlkeq  25373  wwlkexthasheq  25399  wlknwwlknvbij  25405  clwwlkn  25432  clwwlkn2  25440  clwlkisclwwlklem2  25451  clwwlkvbij  25466  eclclwwlkn0  25496  hashecclwwlkn1  25499  usghashecclwwlk  25500  vdgr0  25565  rusgrasn  25610  eupatrl  25633  eupares  25640  vdegp1ai  25649  vdegp1bi  25650  frgra3v  25667  frgrancvvdeqlem9  25706  frgrancvvdgeq  25708  frg2wot1  25722  usgreghash2spotv  25731  extwwlkfablem2  25743  numclwwlkovf2  25749  numclwwlk2lem3  25771  vsfval  26191  ipasslem7  26414  minvecolem2  26454  minvecolem2OLD  26464  h2hcau  26569  h2hlm  26570  hlimadd  26783  hhsscms  26867  chocunii  26891  occllem  26893  leopnmid  27728  opsqrlem1  27730  hmopidmchi  27741  mdslj1i  27909  addltmulALT  28036  imadifxp  28153  xaddeq0  28275  xrge0npcan  28403  gsumle  28488  xrge0tsmsd  28495  locfinreflem  28614  locfinref  28615  xpinpreima2  28660  cnre2csqlem  28663  tpr2rico  28665  ordtrestNEW  28674  ordtrest2NEW  28676  mndpluscn  28679  pnfneige0  28704  qqhghm  28739  qqhrhm  28740  qqhcn  28742  qqhucn  28743  rrhcn  28748  rrhre  28772  esumsplit  28821  esumpr  28834  esumfsup  28838  sigaclcu2  28889  pwsiga  28899  prsiga  28900  sigapildsys  28931  measvuni  28983  elmbfmvol2  29036  mbfmcnt  29037  sxbrsigalem1  29054  sxbrsiga  29059  omsfval  29065  omsfvalOLD  29069  carsgclctunlem2  29098  sibf0  29114  sitgclg  29122  sitmval  29129  eulerpartgbij  29152  eulerpartlemgh  29158  isrrvv  29223  rrvadd  29232  rrvmulc  29233  dstrvprob  29251  coinflipspace  29260  coinfliprv  29262  ballotlemfmpn  29274  ballotlem1ri  29314  ballotlem1riOLD  29352  sgnmulsgn  29367  plymul02  29382  signsplypnf  29386  signsply0  29387  signswrid  29394  indispcon  29904  conpcon  29905  iccllyscon  29920  cvmopnlem  29948  cvmliftlem15  29968  cvmlift2lem3  29975  mrsubff  30097  mrsubccat  30103  circum  30265  elhf2  30886  topdifinfindis  31656  icoreelrn  31671  finxpreclem2  31689  finixpnum  31837  poimirlem5  31852  poimirlem10  31857  poimirlem22  31869  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  poimirlem28  31875  poimirlem29  31876  poimirlem31  31878  poimirlem32  31879  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  ovoliunnfl  31889  voliunnfl  31891  volsupnfl  31892  dvtan  31899  itg2addnclem  31900  ftc1anclem5  31928  dvasin  31935  dvreasin  31937  dvreacos  31938  areacirclem1  31939  areacirc  31944  bnd2lem  32030  prdsbnd  32032  cntotbnd  32035  cnpwstotbnd  32036  isdrngo2  32104  prter2  32364  eqlkr2  32578  tendoidcl  34248  cdlemk56  34450  dihpN  34816  mapdhval  35204  hlhillcs  35441  isnacs3  35464  diophrw  35513  lzenom  35524  diophin  35527  pellexlem5  35590  pw2f1ocnv  35805  dnnumch2  35816  kelac2lem  35835  kelac2  35836  dfac21  35837  pwfi2f1o  35867  frlmpwfi  35869  mpaaeu  35929  rngunsnply  35952  mendbas  35963  mendplusgfval  35964  mendmulrfval  35966  mendsca  35968  mendvscafval  35969  subrgacs  35979  sdrgacs  35980  cntzsdrg  35981  idomodle  35983  phisum  35989  proot1ex  35991  deg1mhm  35997  itgpowd  36012  trclubgNEW  36138  dmtrcl  36147  rntrcl  36148  brfvidRP  36193  trclrelexplem  36216  relexp01min  36218  trclimalb2  36231  amgm2d  36563  amgm3d  36564  amgm4d  36565  hashnzfzclim  36584  ofsubid  36586  ofdivrec  36588  dvconstbi  36596  fzisoeu  37415  iuneqfzuzlem  37454  sumnnodd  37593  negcncfg  37641  cnfdmsn  37642  divcncf  37644  dvmptresicc  37674  itgcoscmulx  37729  stoweidlem13  37756  stoweidlem26  37769  stoweidlem34  37778  stoweidlem42  37786  stoweidlem44  37788  stoweidlem48  37792  stoweidlem62  37806  stoweidlem62OLD  37807  stoweid  37808  stirlinglem7  37825  stirlinglem11  37829  stirlinglem12  37830  dirkeritg  37847  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem16  37868  fourierdlem21  37873  fourierdlem22  37874  fourierdlem24  37876  fourierdlem48  37901  fourierdlem49  37902  fourierdlem62  37915  fourierdlem70  37923  fourierdlem80  37933  fourierdlem83  37936  fourierdlem85  37938  fourierdlem102  37955  fourierdlem104  37957  fourierdlem111  37964  fourierdlem112  37965  fourierdlem114  37967  etransclem18  38000  etransclem23  38005  etransclem24  38006  etransclem25  38007  etransclem35  38017  etransclem46  38028  mod2eq1n2dvds  38538  iccpartipre  38548  iccpartiltu  38549  perfectALTVlem2  38657  stgoldbwt  38690  nnsum3primesgbe  38700  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  bgoldbtbndlem2  38714  snstrvtxval  38911  snstriedgval  38912  uhgrop  38937  uhgrunop  38943  edgastruct  38985  isusgrs  39002  uhgrspan1  39112  upgrres1  39117  umgrres1  39118  usgrres1  39119  fusgredgfi  39127  usgr1v0e  39128  nbgrval  39142  nbusgrf1o1  39180  uvtxa01vtx0  39199  nbupgruvtxres  39208  usgrexi  39234  cusgrexi  39235  cusgrres  39237  cusgrfilem3  39246  sizusglecusg  39252  uhgrepe  39281  uhgres  39282  gordopval  39293  gsizopval  39294  usgedgnlp  39313  isfusgracl  39329  isfusgraclALT  39331  usgo0s0  39338  usgo0s0ALT  39339  usgo1s0ALT  39340  usgo1s0  39345  usgresvm1  39346  usgfis  39349  usgresvm1ALT  39350  usgrafiedgALT  39354  idmgmhm  39379  mgmplusgiopALT  39421  sgrp2sgrp  39455  isrnghm  39483  lidlmmgm  39516  2zrngnmlid  39540  dfrngc2  39565  rnghmsscmap2  39566  rnghmsscmap  39567  rngchomfvalALTV  39577  rngcidALTV  39584  funcrngcsetcALT  39592  dfringc2  39611  rhmsscmap2  39612  rhmsscmap  39613  rhmsscrnghm  39619  rngcresringcat  39623  funcringcsetcALTV2lem8  39636  ringchomfvalALTV  39640  ringcidALTV  39647  funcringcsetclem8ALTV  39659  srhmsubc  39669  fldc  39676  rngcrescrhm  39678  rhmsubclem3  39681  srhmsubcALTV  39688  fldcALTV  39695  rngcrescrhmALTV  39697  altgsumbcALT  39727  zlmodzxzel  39729  zlmodzxzsubm  39733  zlmodzxzsub  39734  gsumpr  39735  scmsuppss  39750  ply1mulgsum  39775  dmatALTbas  39787  lcoop  39797  lincval0  39801  lco0  39813  linds0  39851  snlindsntorlem  39856  lmod1lem2  39874  lmod1lem3  39875  lmod1zr  39879  lmod1zrnlvec  39880  zlmodzxznm  39883  zlmodzxzldeplem4  39889  expnegico01  39908  pw2m1lepw2m1  39911  fldivexpfllog2  39969  blennnelnn  39980  blenpw2  39982  nnpw2pmod  39987  blennnt2  39993  nnolog2flm1  39994  digfval  40001  dignnld  40007  dig2nn0ld  40008  0dig2nn0e  40016  0dig2nn0o  40017
  Copyright terms: Public domain W3C validator