MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp1i Structured version   Visualization version   GIF 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 𝜑
mp1i.2 (𝜑𝜓)
Assertion
Ref Expression
mp1i (𝜒𝜓)

Proof of Theorem mp1i
StepHypRef Expression
1 mp1i.1 . . 3 𝜑
2 mp1i.2 . . 3 (𝜑𝜓)
31, 2ax-mp 5 . 2 𝜓
43a1i 11 1 (𝜒𝜓)
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:  relsnopg  5373  poirr2  5670  fvrnressn  6583  isomin  6742  isoini  6743  mptmpt2opabbrd  7408  supp0  7460  suppval1  7461  suppssr  7487  dmtpos  7525  mpt2curryd  7556  oaabs2  7886  elqsecl  7960  mapsncnv  8062  boxcutc  8109  domunsncan  8217  unxpdom2  8325  sucxpdom  8326  findcard2d  8359  ac6sfi  8361  xpfi  8388  imafi  8416  snopfsupp  8455  fifo  8495  ordtypelem4  8583  oismo  8602  wofib  8607  brwdom2  8635  canthwdom  8641  cantnfval  8730  cantnflt  8734  cantnff  8736  cantnf0  8737  cantnfp1lem1  8740  cantnfp1lem3  8742  cantnflem1b  8748  cantnflem1  8751  cnfcom  8762  cnfcom2lem  8763  ranksnb  8855  tskwe  8958  cardidm  8967  infxpenc  9023  fseqdom  9031  dfac8clem  9037  dfac12lem2  9150  infmap2  9224  isfin4-3  9321  fin23lem14  9339  fin23lem40  9357  isf34lem7  9385  isf34lem6  9386  fin1a2lem12  9417  hsmexlem4  9435  hsmexlem5  9436  ac5b  9484  alephexp1  9585  alephsuc3  9586  fpwwe2lem8  9643  fpwwe2lem13  9648  canthwe  9657  canthp1lem2  9659  gchcda1  9662  pwfseqlem5  9669  wunco  9739  prlem934  10039  supsrlem  10116  msqge0  10733  negfi  11155  ofnegsub  11202  ofsubge0  11203  xaddpnf1  12242  supxrmnf  12332  fz0sn0fz1  12642  injresinjlem  12774  fldiv4lem1div2  12824  uzindi  12967  seqfeq4  13036  seqof  13044  bcval5  13291  hashdomi  13353  hash1snb  13391  hashge2el2difr  13447  hashtpg  13451  fi1uzind  13463  ccatlen  13539  lswccatn0lsw  13555  ccatalpha  13557  eqs1  13575  s111  13578  swrd0  13626  swrdspsleq  13641  wrdeqs1cat  13666  reps  13709  repsw0  13716  repswccat  13724  repswrevw  13725  lswcshw  13753  cshwsexa  13762  scshwfzeqfzo  13764  lsws2  13841  lsws3  13842  lsws4  13843  wrdlen2i  13879  relexpsucnnr  13956  relexpaddg  13984  shftfib  14003  limsupcl  14395  limsupgf  14397  limsupval2  14402  isercolllem3  14588  modfsummods  14716  ackbijnn  14751  supcvg  14779  fprodfac  14894  fprodmodd  14919  fallfac0  14950  bpoly4  14981  ege2le3  15011  rpnnen2lem5  15138  ruclem11  15160  fsumdvds  15224  fproddvdsd  15253  mod2eq1n2dvds  15265  oddnn02np1  15266  oddge22np1  15267  evennn02n  15268  evennn2n  15269  bitsinv2  15359  sadaddlem  15382  smupf  15394  smup0  15395  smu01lem  15401  3lcm2e6woprm  15522  6lcm4e12  15523  lcmfunsnlem1  15544  lcmfunsnlem2lem1  15545  lcmfunsnlem2  15547  coprmprod  15569  isprm6  15620  hashdvds  15674  phisum  15689  reumodprminv  15703  prmreclem6  15819  vdwlem13  15891  ramtlecl  15898  0ram  15918  prmdvdsprmo  15940  fvprmselgcd1  15943  prmgaplcmlem1  15949  prmgaplem7  15955  prmgaplcm  15958  cshwshashnsame  16004  prmlem0  16006  wunndx  16072  prdsval  16309  xpsbas  16428  xpsadd  16430  xpsmul  16431  xpssca  16432  xpsvsca  16433  xpsless  16434  xpsle  16435  mreexexlem2d  16499  mreacs  16512  acsfn  16513  isofn  16628  ciclcl  16655  cicrcl  16656  cicsym  16657  cicer  16659  idfu2nd  16730  idfucl  16734  fucsect  16825  initoeu2lem1  16857  initoeu2lem2  16858  setccatid  16927  setcepi  16931  catchomfval  16941  estrccatid  16965  estrreslem1  16970  estrreslem2  16971  estrres  16972  funcestrcsetclem8  16980  fullestrcsetc  16984  embedsetcestrclem  16990  funcsetcestrclem8  16995  uncfval  17067  oduglb  17332  odumeet  17333  odulub  17334  odujoin  17335  isipodrs  17354  fpwipodrs  17357  isacs5lem  17362  idmhm  17537  submacs  17558  frmdup1  17594  mgmnsgrpex  17611  mulgneg2  17768  subgacs  17822  nsgacs  17823  idrespermg  18023  psgnunilem5  18106  psgnsn  18132  odf1o2  18180  frgpuplem  18377  cygctb  18485  gsumzunsnd  18547  gsum2dlem2  18562  gsummptnn0fz  18574  dprdsubg  18615  dmdprdsplit2lem  18636  dmdprdpr  18640  dprdpr  18641  dpjeq  18650  ablfac1eulem  18663  pgpfac1lem2  18666  pgpfaclem1  18672  srgbinomlem4  18735  unitgrp  18859  isirred  18891  brric  18938  mptscmfsupp0  19122  lssacs  19161  pwssplit1  19253  lbsextlem2  19353  lbsextlem3  19354  isnzr2hash  19458  0ring01eqbi  19467  rng1nnzr  19468  psrass1lem  19571  psrlidm  19597  resspsradd  19610  resspsrmul  19611  resspsrvsca  19612  mplcoe5lem  19661  ltbwe  19666  coe1fsupp  19778  psropprmul  19802  coe1add  19828  coe1mul2lem1  19831  coe1tm  19837  cply1coe0bi  19864  evls1rhmlem  19880  evl1sca  19892  evl1var  19894  pf1mpf  19910  pf1ind  19913  xrsmcmn  19963  xrs1mnd  19978  xrs10  19979  gsumfsum  20007  zringlpir  20031  zringcyg  20033  zndvds  20092  regsumsupp  20162  uvcvv1  20322  lsslinds  20364  matmulr  20438  ofco2  20451  mat0dimbas0  20466  mat1dimelbas  20471  mat1f1o  20478  dmatval  20492  scmatghm  20533  mavmul0  20552  mavmul0g  20553  m1detdiag  20597  mdetunilem9  20620  maducoeval2  20640  madugsum  20643  smadiadetlem0  20661  smadiadetlem1a  20663  smadiadetlem4  20669  smadiadetglem1  20671  smadiadetglem2  20672  smadiadetg  20673  cramer0  20690  cpmat  20708  mat2pmatfval  20722  cpm2mfval  20748  m2cpminvid2lem  20753  pmatcollpw3fi1lem2  20786  pmatcollpw3fi1  20787  idpm2idmp  20800  pm2mpmhmlem2  20818  chpmatfval  20829  chfacfscmulfsupp  20858  chfacfpmmulfsupp  20862  cpmidpmatlem2  20870  cpmadugsumlemF  20875  cpmidgsum2  20878  cpmadumatpolylem1  20880  cayhamlem3  20886  cayhamlem4  20887  indistopon  20999  mreclatdemoBAD  21094  mnfnei  21219  resthauslem  21361  sshauslem  21370  discmp  21395  connima  21422  1stcfb  21442  ptbasfi  21578  hauseqlcld  21643  xkoptsub  21651  xkofvcn  21681  idqtop  21703  tgqtop  21709  kqdisj  21729  xpstopnlem1  21806  xpstopnlem2  21808  ufildom1  21923  alexsubb  22043  alexsubALTlem3  22046  ptcmplem2  22050  ptcmplem3  22051  tmdgsum  22092  ustneism  22220  ustuqtop1  22238  iducn  22280  prdsmet  22368  imasdsf1olem  22371  xpsxmet  22378  xpsdsval  22379  xpsmet  22380  prdsbl  22489  met1stc  22519  prdsxmslem2  22527  xpsxms  22532  xpsms  22533  psmetutop  22565  dscmet  22570  nmoffn  22708  nmofval  22711  nmolb  22714  nmof  22716  cnbl0  22770  xrsmopn  22808  xrge0gsumle  22829  xrge0tsms  22830  negfcncf  22915  cnrehmeo  22945  lebnum  22956  xlebnum  22957  reparphti  22989  pcopt  23014  pcopt2  23015  pcorevcl  23017  pcorevlem  23018  pi1xfrval  23046  pi1xfrcnvlem  23048  pi1xfrcnv  23049  pi1cof  23051  pi1coval  23052  nmhmcn  23112  cphsubrglem  23169  csscld  23240  cmetcaulem  23278  cmpcmet  23308  divcncf  23408  ovolunlem1  23457  ovolicc2lem4  23480  ioovolcl  23530  ioorcl2  23532  uniioovol  23539  uniioombllem4  23546  uniioombllem5  23547  uniioombllem6  23548  dyadmbllem  23559  mbfsub  23620  itg1climres  23672  xrge0f  23689  itg2ge0  23693  itg2i1fseq2  23714  ibl0  23744  ellimc2  23832  limcflf  23836  dvreslem  23864  dvidlem  23870  dvid  23872  cpnres  23891  dvaddbr  23892  dvmulbr  23893  dvfre  23905  dvexp  23907  dvrec  23909  dvmptid  23911  dvmptc  23912  dvmptntr  23925  dvexp3  23932  dvlipcn  23948  dveq0  23954  dv11cn  23955  lhop2  23969  ftc1a  23991  tdeglem1  24009  tdeglem3  24010  tdeglem4  24011  tdeglem2  24012  mdeg0  24021  mdegle0  24028  ply1remlem  24113  plypf1  24159  coe0  24203  dvply1  24230  elqaalem3  24267  aaliou2b  24287  aaliou3lem8  24291  aaliou3lem7  24295  taylfvallem  24303  taylf  24306  tayl0  24307  taylpfval  24310  taylply  24314  dvtaylp  24315  taylthlem1  24318  taylthlem2  24319  ulmdvlem1  24345  ulmdvlem2  24346  ulmdvlem3  24347  radcnvcl  24362  psercnlem2  24369  psercn  24371  pserdv  24374  abelthlem3  24378  abelth  24386  sincn  24389  coscn  24390  reefgim  24395  tangtx  24448  pige3  24460  cosordlem  24468  logcn  24584  dvlog  24588  advlog  24591  advlogexp  24592  logtayl  24597  logccv  24600  dvcxp1  24672  dvcncxp1  24675  cxpcn3lem  24679  cxpcn3  24680  resqrtcn  24681  sqrtcn  24682  loglesqrt  24690  logbfval  24719  logblog  24721  isosctrlem2  24740  dquartlem1  24769  quart  24779  atancj  24828  efiatan  24830  atantan  24841  atanbndlem  24843  atansopn  24850  dvatan  24853  atantayl  24855  leibpilem2  24859  leibpi  24860  log2tlbnd  24863  rlimcnp2  24884  efrlim  24887  divsqrtsumlem  24897  jensenlem1  24904  jensenlem2  24905  jensen  24906  amgmlem  24907  amgm  24908  emcllem4  24916  emcllem7  24919  lgamcvg2  24972  gamcvg2lem  24976  wilthlem2  24986  wilthlem3  24987  basellem6  25003  chtrpcl  25092  ppiltx  25094  1sgm2ppw  25116  chtlepsi  25122  chpub  25136  logfacbnd3  25139  logfacrlim  25140  perfectlem2  25146  dchrelbas2  25153  dchrabs  25176  dchrhash  25187  bposlem7  25206  lgsdir2lem5  25245  lgsqrlem1  25262  gausslemma2dlem5  25287  gausslemma2dlem6  25288  lgseisenlem4  25294  lgsquad2lem1  25300  lgsquad3  25303  chpo1ub  25360  vmadivsumb  25363  rpvmasumlem  25367  dchrisumlem2  25370  dchrmusumlema  25373  dchrvmasumlem2  25378  dchrvmasumlema  25380  dchrvmasumiflem1  25381  dchrisum0flblem1  25388  dchrisum0lem1  25396  rplogsum  25407  mudivsum  25410  logdivsum  25413  mulog2sumlem2  25415  vmalogdivsum2  25418  2vmadivsumlem  25420  log2sumbnd  25424  selberglem2  25426  selbergb  25429  selberg2lem  25430  selberg2b  25432  selberg3lem1  25437  selberg4lem1  25440  selberg4  25441  pntrsumo1  25445  pntrlog2bndlem2  25458  pntrlog2bndlem3  25459  pntrlog2bndlem4  25460  pntrlog2bndlem5  25461  pntibndlem1  25469  pntibndlem2  25471  pntibndlem3  25472  pntlemb  25477  pntlemr  25482  pntlemf  25485  pntlem3  25489  pnt  25494  qabvle  25505  padicabv  25510  ostth1  25513  istrkg2ld  25550  tgldimor  25588  tgcgr4  25617  motgrp  25629  perpln1  25796  perpln2  25797  isperp  25798  snstrvtxval  26120  snstriedgval  26121  isuhgrop  26156  uhgrunop  26161  uhgrstrrepe  26164  upgrop  26180  upgrunop  26205  umgrunop  26207  isusgrs  26242  isuspgrop  26247  isusgrop  26248  usgrop  26249  usgrstrrepe  26318  uspgr1ewop  26331  usgr2v1e2w  26335  uhgrspan1  26386  upgrres  26389  umgrres  26390  usgrres  26391  upgrres1  26396  umgrres1  26397  usgrres1  26398  isfusgrcl  26404  fusgredgfi  26408  usgr1v0e  26409  nbgrval  26420  nbusgrf1o1  26462  nbfusgrlevtxm2  26470  uvtx01vtx  26492  uvtxa01vtx0OLD  26494  usgrexilem  26538  usgrexi  26539  cusgrexi  26541  structtousgr  26543  structtocusgr  26544  cusgrres  26546  cusgrfilem3  26555  sizusglecusg  26561  vtxdgfval  26565  vtxdgop  26568  vtxdgf  26569  vtxdlfgrval  26583  vtxd0nedgb  26586  vtxdusgr0edgnelALT  26594  1loopgrvd0  26602  1egrvtxdg1  26607  1egrvtxdg0  26609  p1evtxdeqlem  26610  p1evtxdeq  26611  p1evtxdp1  26612  umgr2v2e  26623  vdiscusgrb  26628  vdegp1ai  26634  vdegp1bi  26635  ewlkle  26703  wksfval  26707  wksv  26717  wlk1ewlk  26738  uspgr2wlkeq  26744  wlkp1lem8  26779  upgr2pthnlp  26830  wlkiswwlks2  26976  wlksnwwlknvbij  27018  2pthdlem1  27042  wpthswwlks2on  27074  elwwlks2  27080  clwlkclwwlklem1  27114  clwwlknfi  27166  hashecclwwlkn1  27200  umgrhashecclwwlk  27201  clwwlkvbij  27254  clwwlkvbijOLD  27255  0wlkonlem1  27262  0wlkons1  27265  0pthon  27271  3wlkdlem4  27306  upgr3v3e3cycl  27324  trlsegvdeglem3  27366  trlsegvdeglem5  27368  eupth2lemb  27381  frgr3v  27421  frgr2wwlk1  27475  fusgreghash2wspv  27481  ex-lcm  27618  vsfval  27789  ipasslem7  27992  minvecolem2  28032  h2hcau  28137  h2hlm  28138  hlimadd  28351  hhsscms  28437  chocunii  28461  occllem  28463  leopnmid  29298  opsqrlem1  29300  hmopidmchi  29311  mdslj1i  29479  addltmulALT  29606  imadifxp  29713  xaddeq0  29819  fzodif2  29853  xrge0npcan  29995  gsumle  30080  xrge0tsmsd  30086  locfinreflem  30208  locfinref  30209  xpinpreima2  30254  cnre2csqlem  30257  tpr2rico  30259  ordtrestNEW  30268  ordtrest2NEW  30270  mndpluscn  30273  pnfneige0  30298  qqhghm  30333  qqhrhm  30334  qqhcn  30336  qqhucn  30337  rrhcn  30342  rrhre  30366  esumsplit  30416  esumpr  30429  esumfsup  30433  sigaclcu2  30484  pwsiga  30494  prsiga  30495  sigapildsys  30526  ldgenpisyslem1  30527  measvuni  30578  elmbfmvol2  30630  mbfmcnt  30631  sxbrsigalem1  30648  sxbrsiga  30653  omsfval  30657  carsgclctunlem2  30682  sibf0  30697  sitgclg  30705  sitmval  30712  eulerpartgbij  30735  eulerpartlemgh  30741  isrrvv  30806  rrvadd  30815  rrvmulc  30816  dstrvprob  30834  coinflipspace  30843  coinfliprv  30845  ballotlemfmpn  30857  ballotlem1ri  30897  sgnmulsgn  30912  plymul02  30924  signsplypnf  30928  signsply0  30929  signswrid  30936  prodfzo03  30982  itgexpif  30985  circlemethhgt  31022  hgt750lemb  31035  indispconn  31515  connpconn  31516  iccllysconn  31531  cvmopnlem  31559  cvmliftlem15  31579  cvmlift2lem3  31586  mrsubff  31708  mrsubccat  31714  circum  31867  noextend  32117  nosupbnd2lem1  32159  elhf2  32580  topdifinfindis  33497  icoreelrn  33512  finxpreclem2  33530  finixpnum  33699  matunitlindflem1  33710  matunitlindflem2  33711  poimirlem5  33719  poimirlem10  33724  poimirlem22  33736  poimirlem26  33740  poimirlem27  33741  poimirlem28  33742  poimirlem29  33743  poimirlem31  33745  poimirlem32  33746  mblfinlem3  33753  mblfinlem4  33754  ismblfin  33755  ovoliunnfl  33756  voliunnfl  33758  volsupnfl  33759  dvtan  33765  itg2addnclem  33766  ftc1anclem5  33794  dvasin  33801  dvreasin  33803  dvreacos  33804  areacirclem1  33805  areacirc  33810  bnd2lem  33895  prdsbnd  33897  cntotbnd  33900  cnpwstotbnd  33901  isdrngo2  34062  prter2  34662  eqlkr2  34882  tendoidcl  36551  cdlemk56  36753  dihpN  37119  mapdhval  37507  hlhillcs  37744  isnacs3  37767  diophrw  37816  lzenom  37827  diophin  37830  pellexlem5  37891  pw2f1ocnv  38098  dnnumch2  38109  kelac2lem  38128  kelac2  38129  dfac21  38130  pwfi2f1o  38160  frlmpwfi  38162  mpaaeu  38214  rngunsnply  38237  mendbas  38248  mendplusgfval  38249  mendmulrfval  38251  mendsca  38253  mendvscafval  38254  subrgacs  38264  sdrgacs  38265  cntzsdrg  38266  idomodle  38268  proot1ex  38273  deg1mhm  38279  itgpowd  38294  trclubgNEW  38419  dmtrcl  38428  rntrcl  38429  brfvidRP  38474  trclrelexplem  38497  relexp01min  38499  trclimalb2  38512  dssmapfvd  38805  ntrk0kbimka  38831  ntrrn  38914  dssmapntrcls  38920  amgm2d  38995  amgm3d  38996  amgm4d  38997  hashnzfzclim  39015  ofsubid  39017  ofdivrec  39019  dvconstbi  39027  fzisoeu  40005  iuneqfzuzlem  40040  sumnnodd  40357  liminfgf  40485  negcncfg  40589  cnfdmsn  40590  dvmptresicc  40629  itgcoscmulx  40680  stoweidlem13  40725  stoweidlem26  40738  stoweidlem34  40746  stoweidlem42  40754  stoweidlem44  40756  stoweidlem48  40760  stoweidlem62  40774  stoweid  40775  stirlinglem7  40792  stirlinglem11  40796  stirlinglem12  40797  dirkeritg  40814  dirkercncflem2  40816  dirkercncflem4  40818  fourierdlem16  40835  fourierdlem21  40840  fourierdlem22  40841  fourierdlem24  40843  fourierdlem48  40866  fourierdlem49  40867  fourierdlem62  40880  fourierdlem70  40888  fourierdlem80  40898  fourierdlem83  40901  fourierdlem85  40903  fourierdlem102  40920  fourierdlem104  40922  fourierdlem111  40929  fourierdlem112  40930  fourierdlem114  40932  etransclem18  40964  etransclem23  40969  etransclem24  40970  etransclem25  40971  etransclem35  40981  etransclem46  40992  ovolval5lem3  41366  setsidel  41848  iccpartipre  41859  iccpartiltu  41860  fmtnoprmfac2lem1  41980  mod42tp1mod8  42021  sfprmdvdsmersenne  42022  perfectALTVlem2  42133  stgoldbwt  42166  nnsum3primesgbe  42182  nnsum4primesodd  42186  nnsum4primesoddALTV  42187  nnsum4primeseven  42190  nnsum4primesevenALTV  42191  bgoldbtbndlem2  42196  upwlksfval  42218  sprval  42231  sprbisymrel  42251  uspgrbisymrelALT  42265  idmgmhm  42290  mgmplusgiopALT  42332  sgrp2sgrp  42366  isrnghm  42394  lidlmmgm  42427  2zrngnmlid  42451  dfrngc2  42474  rnghmsscmap2  42475  rnghmsscmap  42476  rngchomfvalALTV  42486  rngcidALTV  42493  funcrngcsetcALT  42501  dfringc2  42520  rhmsscmap2  42521  rhmsscmap  42522  rhmsscrnghm  42528  rngcresringcat  42532  funcringcsetcALTV2lem8  42545  ringchomfvalALTV  42549  ringcidALTV  42556  funcringcsetclem8ALTV  42568  srhmsubc  42578  fldc  42585  rngcrescrhm  42587  rhmsubclem3  42590  srhmsubcALTV  42596  fldcALTV  42603  rngcrescrhmALTV  42605  altgsumbcALT  42633  zlmodzxzel  42635  zlmodzxzsubm  42639  zlmodzxzsub  42640  gsumpr  42641  scmsuppss  42655  ply1mulgsum  42680  dmatALTbas  42692  lcoop  42702  lincval0  42706  lco0  42718  linds0  42756  snlindsntorlem  42761  lmod1lem2  42779  lmod1lem3  42780  lmod1zr  42784  lmod1zrnlvec  42785  zlmodzxznm  42788  zlmodzxzldeplem4  42794  expnegico01  42810  pw2m1lepw2m1  42812  fldivexpfllog2  42861  blennnelnn  42872  blenpw2  42874  nnpw2pmod  42879  blennnt2  42885  nnolog2flm1  42886  digfval  42893  dignnld  42899  dig2nn0ld  42900  0dig2nn0e  42908  0dig2nn0o  42909  amgmwlem  43053  amgmlemALT  43054  amgmw2d  43055
  Copyright terms: Public domain W3C validator