MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp1i Structured version   Visualization 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  5243  relcoi2  5382  fvrnressn  6103  isomin  6253  isoini  6254  supp0  6946  suppval1  6947  suppssr  6973  dmtpos  7011  mpt2curryd  7042  oaabs2  7372  mapsncnv  7544  boxcutc  7591  domunsncan  7698  pw2f1o  7703  unxpdom2  7806  sucxpdom  7807  findcard2d  7839  ac6sfi  7841  xpfi  7868  imafi  7893  snopfsupp  7932  fifo  7972  ordtypelem4  8062  oismo  8081  wofib  8086  brwdom2  8114  canthwdom  8120  cantnfval  8199  cantnflt  8203  cantnff  8205  cantnf0  8206  cantnfp1lem1  8209  cantnfp1lem3  8211  cantnflem1b  8217  cantnflem1  8220  cnfcom  8231  cnfcom2lem  8232  ranksnb  8324  tskwe  8410  cardidm  8419  infxpenc  8475  fseqdom  8483  dfac8clem  8489  dfac12lem2  8600  infmap2  8674  isfin4-3  8771  fin23lem14  8789  fin23lem40  8807  isf34lem7  8835  isf34lem6  8836  fin1a2lem12  8867  hsmexlem4  8885  hsmexlem5  8886  ac5b  8934  alephexp1  9030  alephsuc3  9031  fpwwe2lem8  9088  fpwwe2lem13  9093  canthwe  9102  canthp1lem2  9104  gchcda1  9107  pwfseqlem5  9114  wunco  9184  prlem934  9484  supsrlem  9561  msqge0  10163  negfi  10582  ofnegsub  10635  ofsubge0  10636  xaddpnf1  11548  supxrmnf  11632  injresinjlem  12056  uzindi  12226  seqfeq4  12294  seqof  12302  bcval5  12535  hashdomi  12591  hash1snb  12626  hashge2el2difr  12671  fi1uzind  12683  ccatlen  12757  lswccatn0lsw  12770  eqs1  12786  s111  12789  swrd0  12827  swrdspsleq  12842  wrdeqs1cat  12868  reps  12910  repsw0  12917  repswccat  12925  repswrevw  12926  lswcshw  12951  cshwsexa  12960  scshwfzeqfzo  12962  lsws2  13035  lsws3  13036  lsws4  13037  wrdlen2i  13067  relexpsucnnr  13137  relexpaddg  13165  shftfib  13184  limsupcl  13578  limsupclOLD  13579  limsupgf  13582  limsupval2  13589  limsupval2OLD  13590  isercolllem3  13779  modfsummods  13902  ackbijnn  13935  supcvg  13963  fprodfac  14076  fallfac0  14130  bpoly4  14161  ege2le3  14193  rpnnen2lem5  14320  ruclem11  14341  fsumdvds  14397  bitsinv2  14466  sadaddlem  14489  smupf  14501  smup0  14502  smu01lem  14508  3lcm2e6woprm  14629  6lcm4e12  14630  lcmslefacOLD  14635  lcmfunsnlem1  14659  lcmfunsnlem2lem1  14660  lcmfunsnlem2  14662  isprm6  14715  coprmprod  14727  hashdvds  14772  reumodprminv  14804  prmreclem6  14914  vdwlem13  14992  ramtlecl  15000  0ram  15027  prmdvdsprmo  15049  fvprmselgcd1  15052  prmgaplcmlem1  15058  prmgaplcmlem1OLD  15061  prmdvdsprmorOLD  15064  prmgaplem7  15076  prmgaplcm  15080  cshwshashnsame  15123  prmlem0  15126  wunndx  15186  prdsval  15402  xpsbas  15529  xpsadd  15531  xpsmul  15532  xpssca  15533  xpsvsca  15534  xpsless  15535  xpsle  15536  mreexexlem2d  15600  mreacs  15613  acsfn  15614  isofn  15729  ciclcl  15756  cicrcl  15757  cicsym  15758  cicer  15760  idfu2nd  15831  idfucl  15835  fucsect  15926  initoeu2lem1  15958  initoeu2lem2  15959  setccatid  16028  setcepi  16032  catchomfval  16042  estrccatid  16066  estrreslem1  16071  estrreslem2  16072  estrres  16073  funcestrcsetclem8  16081  fullestrcsetc  16085  embedsetcestrclem  16091  funcsetcestrclem8  16096  uncfval  16168  oduglb  16434  odumeet  16435  odulub  16436  odujoin  16437  isipodrs  16456  fpwipodrs  16459  isacs4lem  16463  isacs5lem  16464  idmhm  16640  submacs  16661  frmdup1  16697  mgmnsgrpex  16714  mulgneg2  16834  subgacs  16901  nsgacs  16902  idrespermg  17101  psgnunilem5  17184  psgnsn  17210  odf1o2  17271  frgpuplem  17471  cygctb  17575  gsumzunsnd  17637  gsum2dlem2  17652  gsummptnn0fz  17664  dprdsubg  17706  dmdprdsplit2lem  17727  dmdprdpr  17731  dprdpr  17732  dpjeq  17741  ablfac1eulem  17754  pgpfac1lem2  17757  pgpfaclem1  17763  srgbinomlem4  17825  unitgrp  17944  isirred  17976  brric  18021  mptscmfsupp0  18202  lssacs  18239  pwssplit1  18331  lbsextlem2  18431  lbsextlem3  18432  isnzr2hash  18537  0ring01eqbi  18546  rng1nnzr  18547  psrass1lem  18650  psrlidm  18676  resspsradd  18689  resspsrmul  18690  resspsrvsca  18691  mplcoe5lem  18740  ltbwe  18745  coe1fsupp  18856  psropprmul  18880  coe1add  18906  coe1mul2lem1  18909  coe1tm  18915  cply1coe0bi  18943  evls1rhmlem  18959  evl1sca  18971  evl1var  18973  pf1mpf  18989  pf1ind  18992  xrsmcmn  19040  xrs1mnd  19055  xrs10  19056  gsumfsum  19083  zringlpir  19107  zringlpirOLD  19108  zringcyg  19109  zndvds  19169  regsumsupp  19239  uvcvv1  19396  lsslinds  19438  matmulr  19512  ofco2  19525  mat0dimbas0  19540  mat1dimelbas  19545  mat1f1o  19552  dmatval  19566  scmatghm  19607  mavmul0  19626  mavmul0g  19627  m1detdiag  19671  mdetunilem9  19694  maducoeval2  19714  madugsum  19717  smadiadetlem0  19735  smadiadetlem1a  19737  smadiadetlem4  19743  smadiadetglem1  19745  smadiadetglem2  19746  smadiadetg  19747  cramer0  19764  cpmat  19782  mat2pmatfval  19796  cpm2mfval  19822  m2cpminvid2lem  19827  pmatcollpw3fi1lem2  19860  pmatcollpw3fi1  19861  idpm2idmp  19874  pm2mpmhmlem2  19892  chpmatfval  19903  chfacfscmulfsupp  19932  chfacfpmmulfsupp  19936  cpmidpmatlem2  19944  cpmadugsumlemF  19949  cpmidgsum2  19952  cpmadumatpolylem1  19954  cayhamlem3  19960  cayhamlem4  19961  indistopon  20065  mreclatdemoBAD  20161  mnfnei  20286  resthauslem  20428  sshauslem  20437  discmp  20462  conima  20489  1stcfb  20509  hauseqlcld  20710  xkoptsub  20718  xkofvcn  20748  idqtop  20770  tgqtop  20776  kqdisj  20796  xpstopnlem1  20873  xpstopnlem2  20875  ufildom1  20990  alexsubb  21110  alexsubALTlem3  21113  ptcmplem2  21117  ptcmplem3  21118  tmdgsum  21159  ustneism  21287  ustuqtop1  21305  iducn  21347  prdsmet  21434  imasdsf1olem  21437  xpsxmet  21444  xpsdsval  21445  xpsmet  21446  prdsbl  21555  met1stc  21585  prdsxmslem2  21593  xpsxms  21598  xpsms  21599  psmetutop  21631  dscmet  21636  nmoffn  21765  nmofval  21768  nmolb  21771  nmof  21773  nmoffnOLD  21786  nmofvalOLD  21787  nmolbOLD  21790  nmofOLD  21791  cnbl0  21843  xrsmopn  21879  xrge0gsumle  21900  xrge0tsms  21901  negfcncf  22000  cnrehmeo  22030  lebnum  22044  xlebnum  22045  reparphti  22077  pcopt  22102  pcopt2  22103  pcorevcl  22105  pcorevlem  22106  pi1xfrval  22134  pi1xfrcnvlem  22136  pi1xfrcnv  22137  pi1cof  22139  pi1coval  22140  nmhmcn  22183  cphsubrglem  22204  csscld  22269  cmetcaulem  22307  cmpcmet  22336  ovolunlem1  22499  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ioovolcl  22571  ioorcl2  22573  uniioovol  22585  uniioombllem4  22593  uniioombllem5  22594  uniioombllem6  22595  dyadmbllem  22606  mbfsub  22667  itg1climres  22721  xrge0f  22738  itg2ge0  22742  itg2i1fseq2  22763  ibl0  22793  ellimc2  22881  limcflf  22885  dvreslem  22913  dvidlem  22919  dvid  22921  cpnres  22940  dvaddbr  22941  dvmulbr  22942  dvfre  22954  dvexp  22956  dvrec  22958  dvmptid  22960  dvmptc  22961  dvmptntr  22974  dvexp3  22979  dvlipcn  22995  dveq0  23001  dv11cn  23002  lhop2  23016  ftc1a  23038  tdeglem1  23056  tdeglem3  23057  tdeglem4  23058  tdeglem2  23059  mdeg0  23068  mdegle0  23075  ply1remlem  23162  fta1glem2  23166  plypf1  23215  coe0  23259  dvply1  23286  elqaalem3  23323  elqaalem3OLD  23326  aaliou2b  23346  aaliou3lem8  23350  aaliou3lem7  23354  taylfvallem  23362  taylf  23365  tayl0  23366  taylpfval  23369  taylply  23373  dvtaylp  23374  taylthlem1  23377  taylthlem2  23378  ulmdvlem1  23404  ulmdvlem2  23405  ulmdvlem3  23406  radcnvcl  23421  psercnlem2  23428  psercn  23430  pserdv  23433  abelthlem3  23437  abelth  23445  sincn  23448  coscn  23449  reefgim  23454  tangtx  23509  pige3  23521  cosordlem  23529  logcn  23641  dvlog  23645  advlog  23648  advlogexp  23649  logtayl  23654  logccv  23657  dvcxp1  23729  dvcncxp1  23732  cxpcn3lem  23736  cxpcn3  23737  resqrtcn  23738  sqrtcn  23739  loglesqrt  23747  logbfval  23776  logblog  23778  isosctrlem2  23797  dquartlem1  23826  quart  23836  atancj  23885  efiatan  23887  atantan  23898  atanbndlem  23900  atansopn  23907  dvatan  23910  atantayl  23912  leibpilem2  23916  leibpi  23917  log2tlbnd  23920  rlimcnp2  23941  efrlim  23944  divsqrtsumlem  23954  jensenlem1  23961  jensenlem2  23962  jensen  23963  amgmlem  23964  amgm  23965  emcllem4  23973  emcllem7  23976  lgamcvg2  24029  gamcvg2lem  24033  wilthlem2  24043  wilthlem3  24044  basellem6  24061  chtrpcl  24151  ppiltx  24153  1sgm2ppw  24177  chtlepsi  24183  chpub  24197  logfacbnd3  24200  logfacrlim  24201  perfectlem2  24207  dchrelbas2  24214  dchrabs  24237  dchrhash  24248  bposlem7  24267  lgsdir2lem5  24304  lgsqrlem1  24318  lgseisenlem4  24329  lgsquad2lem1  24335  lgsquad3  24338  chpo1ub  24367  vmadivsumb  24370  rpvmasumlem  24374  dchrisumlem2  24377  dchrmusumlema  24380  dchrvmasumlem2  24385  dchrvmasumlema  24387  dchrvmasumiflem1  24388  dchrisum0flblem1  24395  dchrisum0lem1  24403  rplogsum  24414  mudivsum  24417  logdivsum  24420  mulog2sumlem2  24422  vmalogdivsum2  24425  2vmadivsumlem  24427  log2sumbnd  24431  selberglem2  24433  selbergb  24436  selberg2lem  24437  selberg2b  24439  selberg3lem1  24444  selberg4lem1  24447  selberg4  24448  pntrsumo1  24452  pntrlog2bndlem2  24465  pntrlog2bndlem3  24466  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  pntibndlem1  24476  pntibndlem2  24478  pntibndlem3  24479  pntlemb  24484  pntlemr  24489  pntlemf  24492  pntlem3  24496  pnt  24501  qabvle  24512  padicabv  24517  ostth1  24520  istrkg2ld  24557  tgldimor  24595  tgcgr4  24625  motgrp  24637  perpln1  24804  perpln2  24805  isperp  24806  uhgrares  25084  umgrares  25100  edgopval  25116  usgrares  25145  nbgraop  25200  nbgraopALT  25201  nbgraf1o0  25223  cusgra0v  25237  cusgra1v  25238  cusgraexilem2  25244  sizeusglecusg  25263  isuvtx  25265  2trllemH  25331  wlkntrllem3  25340  2wlklem1  25376  usgra2wlkspthlem1  25396  usgra2wlkspthlem2  25397  constr3trllem3  25429  constr3pthlem3  25434  wwlkn  25459  wlkiswwlk2  25474  wwlkn0s  25482  usg2wlkeq  25485  wwlkexthasheq  25511  wlknwwlknvbij  25517  clwwlkn  25544  clwwlkn2  25552  clwlkisclwwlklem2  25563  clwwlkvbij  25578  eclclwwlkn0  25608  hashecclwwlkn1  25611  usghashecclwwlk  25612  vdgr0  25677  rusgrasn  25722  eupatrl  25745  eupares  25752  vdegp1ai  25761  vdegp1bi  25762  frgra3v  25779  frgrancvvdeqlem9  25818  frgrancvvdgeq  25820  frg2wot1  25834  usgreghash2spotv  25843  extwwlkfablem2  25855  numclwwlkovf2  25861  numclwwlk2lem3  25883  vsfval  26303  ipasslem7  26526  minvecolem2  26566  minvecolem2OLD  26576  h2hcau  26681  h2hlm  26682  hlimadd  26895  hhsscms  26979  chocunii  27003  occllem  27005  leopnmid  27840  opsqrlem1  27842  hmopidmchi  27853  mdslj1i  28021  addltmulALT  28148  imadifxp  28261  xaddeq0  28379  xrge0npcan  28506  gsumle  28591  xrge0tsmsd  28597  locfinreflem  28716  locfinref  28717  xpinpreima2  28762  cnre2csqlem  28765  tpr2rico  28767  ordtrestNEW  28776  ordtrest2NEW  28778  mndpluscn  28781  pnfneige0  28806  qqhghm  28841  qqhrhm  28842  qqhcn  28844  qqhucn  28845  rrhcn  28850  rrhre  28874  esumsplit  28923  esumpr  28936  esumfsup  28940  sigaclcu2  28991  pwsiga  29001  prsiga  29002  sigapildsys  29033  measvuni  29085  elmbfmvol2  29138  mbfmcnt  29139  sxbrsigalem1  29156  sxbrsiga  29161  omsfval  29167  omsfvalOLD  29171  carsgclctunlem2  29200  sibf0  29216  sitgclg  29224  sitmval  29231  eulerpartgbij  29254  eulerpartlemgh  29260  isrrvv  29325  rrvadd  29334  rrvmulc  29335  dstrvprob  29353  coinflipspace  29362  coinfliprv  29364  ballotlemfmpn  29376  ballotlem1ri  29416  ballotlem1riOLD  29454  sgnmulsgn  29469  plymul02  29484  signsplypnf  29488  signsply0  29489  signswrid  29496  indispcon  30006  conpcon  30007  iccllyscon  30022  cvmopnlem  30050  cvmliftlem15  30070  cvmlift2lem3  30077  mrsubff  30199  mrsubccat  30205  circum  30367  elhf2  30991  topdifinfindis  31794  icoreelrn  31809  finxpreclem2  31827  finixpnum  31975  poimirlem5  31990  poimirlem10  31995  poimirlem22  32007  poimirlem25  32010  poimirlem26  32011  poimirlem27  32012  poimirlem28  32013  poimirlem29  32014  poimirlem31  32016  poimirlem32  32017  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  ovoliunnfl  32027  voliunnfl  32029  volsupnfl  32030  dvtan  32037  itg2addnclem  32038  ftc1anclem5  32066  dvasin  32073  dvreasin  32075  dvreacos  32076  areacirclem1  32077  areacirc  32082  bnd2lem  32168  prdsbnd  32170  cntotbnd  32173  cnpwstotbnd  32174  isdrngo2  32242  prter2  32498  eqlkr2  32711  tendoidcl  34381  cdlemk56  34583  dihpN  34949  mapdhval  35337  hlhillcs  35574  isnacs3  35597  diophrw  35646  lzenom  35657  diophin  35660  pellexlem5  35722  pw2f1ocnv  35937  dnnumch2  35948  kelac2lem  35967  kelac2  35968  dfac21  35969  pwfi2f1o  35999  frlmpwfi  36001  mpaaeu  36061  rngunsnply  36084  mendbas  36095  mendplusgfval  36096  mendmulrfval  36098  mendsca  36100  mendvscafval  36101  subrgacs  36111  sdrgacs  36112  cntzsdrg  36113  idomodle  36115  phisum  36121  proot1ex  36123  deg1mhm  36129  itgpowd  36144  trclubgNEW  36270  dmtrcl  36279  rntrcl  36280  brfvidRP  36325  trclrelexplem  36348  relexp01min  36350  trclimalb2  36363  amgm2d  36694  amgm3d  36695  amgm4d  36696  hashnzfzclim  36715  ofsubid  36717  ofdivrec  36719  dvconstbi  36727  fzisoeu  37556  iuneqfzuzlem  37595  sumnnodd  37748  negcncfg  37796  cnfdmsn  37797  divcncf  37799  dvmptresicc  37829  itgcoscmulx  37884  stoweidlem13  37911  stoweidlem26  37924  stoweidlem34  37933  stoweidlem42  37941  stoweidlem44  37943  stoweidlem48  37947  stoweidlem62  37961  stoweidlem62OLD  37962  stoweid  37963  stirlinglem7  37980  stirlinglem11  37984  stirlinglem12  37985  dirkeritg  38002  dirkercncflem2  38004  dirkercncflem4  38006  fourierdlem16  38023  fourierdlem21  38028  fourierdlem22  38029  fourierdlem24  38031  fourierdlem48  38056  fourierdlem49  38057  fourierdlem62  38070  fourierdlem70  38078  fourierdlem80  38088  fourierdlem83  38091  fourierdlem85  38093  fourierdlem102  38110  fourierdlem104  38112  fourierdlem111  38119  fourierdlem112  38120  fourierdlem114  38122  etransclem18  38155  etransclem23  38160  etransclem24  38161  etransclem25  38162  etransclem35  38172  etransclem46  38183  mod2eq1n2dvds  38763  iccpartipre  38773  iccpartiltu  38774  perfectALTVlem2  38882  stgoldbwt  38915  nnsum3primesgbe  38925  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  bgoldbtbndlem2  38939  mptmpt2opabbrd  39076  snstrvtxval  39183  snstriedgval  39184  isuhgrop  39210  uhgrunop  39215  edgastruct  39263  isusgrs  39291  isusgrop  39297  usgrop  39298  uspgr1ewop  39373  usgr2v1e2w  39377  uhgrspan1  39425  upgrres1  39430  umgrres1  39431  usgrres1  39432  fusgredgfi  39441  usgr1v0e  39442  nbgrval  39456  nbusgrf1o1  39494  nbfusgrlevtxm2  39502  uvtxa01vtx0  39519  nbupgruvtxres  39530  usgrexi  39556  cusgrexi  39557  cusgrres  39559  cusgrfilem3  39568  sizusglecusg  39574  vtxdgfval  39578  vtxdgf  39581  vtxdumgrval  39590  uhgrvd0nedgb  39595  vtxdusgr0edgnelALT  39600  umgr2v2eedg  39611  umgr2v2e  39612  vdiscusgrb  39617  ewlkle  39672  1wlksfval  39674  wlksfval  39675  1wlksv  39683  1wlk1ewlk  39698  upgr2pthnlp  39765  0wlkOnlem1  39835  2pthdlem1  39879  31wlkdlem4  39903  upgr3v3e3cycl  39921  uhgrepe  39963  uhgres  39964  gordopval  39975  gsizopval  39976  usgedgnlp  39995  isfusgracl  40011  isfusgraclALT  40013  usgo0s0  40020  usgo0s0ALT  40021  usgo1s0ALT  40022  usgo1s0  40027  usgresvm1  40028  usgfis  40031  usgresvm1ALT  40032  usgrafiedgALT  40036  idmgmhm  40061  mgmplusgiopALT  40103  sgrp2sgrp  40137  isrnghm  40165  lidlmmgm  40198  2zrngnmlid  40222  dfrngc2  40247  rnghmsscmap2  40248  rnghmsscmap  40249  rngchomfvalALTV  40259  rngcidALTV  40266  funcrngcsetcALT  40274  dfringc2  40293  rhmsscmap2  40294  rhmsscmap  40295  rhmsscrnghm  40301  rngcresringcat  40305  funcringcsetcALTV2lem8  40318  ringchomfvalALTV  40322  ringcidALTV  40329  funcringcsetclem8ALTV  40341  srhmsubc  40351  fldc  40358  rngcrescrhm  40360  rhmsubclem3  40363  srhmsubcALTV  40370  fldcALTV  40377  rngcrescrhmALTV  40379  altgsumbcALT  40407  zlmodzxzel  40409  zlmodzxzsubm  40413  zlmodzxzsub  40414  gsumpr  40415  scmsuppss  40430  ply1mulgsum  40455  dmatALTbas  40467  lcoop  40477  lincval0  40481  lco0  40493  linds0  40531  snlindsntorlem  40536  lmod1lem2  40554  lmod1lem3  40555  lmod1zr  40559  lmod1zrnlvec  40560  zlmodzxznm  40563  zlmodzxzldeplem4  40569  expnegico01  40588  pw2m1lepw2m1  40591  fldivexpfllog2  40649  blennnelnn  40660  blenpw2  40662  nnpw2pmod  40667  blennnt2  40673  nnolog2flm1  40674  digfval  40681  dignnld  40687  dig2nn0ld  40688  0dig2nn0e  40696  0dig2nn0o  40697
  Copyright terms: Public domain W3C validator