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:  poirr2  5423  fvrnressn  6308  isomin  6462  isoini  6463  supp0  7161  suppval1  7162  suppssr  7187  dmtpos  7225  mpt2curryd  7256  oaabs2  7586  elqsecl  7662  mapsncnv  7764  boxcutc  7811  domunsncan  7919  unxpdom2  8027  sucxpdom  8028  findcard2d  8061  ac6sfi  8063  xpfi  8090  imafi  8116  snopfsupp  8155  fifo  8195  ordtypelem4  8283  oismo  8302  wofib  8307  brwdom2  8335  canthwdom  8341  cantnfval  8422  cantnflt  8426  cantnff  8428  cantnf0  8429  cantnfp1lem1  8432  cantnfp1lem3  8434  cantnflem1b  8440  cantnflem1  8443  cnfcom  8454  cnfcom2lem  8455  ranksnb  8547  tskwe  8633  cardidm  8642  infxpenc  8698  fseqdom  8706  dfac8clem  8712  dfac12lem2  8823  infmap2  8897  isfin4-3  8994  fin23lem14  9012  fin23lem40  9030  isf34lem7  9058  isf34lem6  9059  fin1a2lem12  9090  hsmexlem4  9108  hsmexlem5  9109  ac5b  9157  alephexp1  9254  alephsuc3  9255  fpwwe2lem8  9312  fpwwe2lem13  9317  canthwe  9326  canthp1lem2  9328  gchcda1  9331  pwfseqlem5  9338  wunco  9408  prlem934  9708  supsrlem  9785  msqge0  10395  negfi  10817  ofnegsub  10862  ofsubge0  10863  xaddpnf1  11887  supxrmnf  11972  fz0sn0fz1  12277  injresinjlem  12402  fldiv4lem1div2  12452  uzindi  12595  seqfeq4  12664  seqof  12672  bcval5  12919  hashdomi  12979  hash1snb  13017  hashge2el2difr  13065  hashtpg  13068  fi1uzind  13077  fi1uzindOLD  13083  ccatlen  13156  lswccatn0lsw  13169  ccatalpha  13171  eqs1  13188  s111  13191  swrd0  13229  swrdspsleq  13244  wrdeqs1cat  13269  reps  13311  repsw0  13318  repswccat  13326  repswrevw  13327  lswcshw  13355  cshwsexa  13364  scshwfzeqfzo  13366  lsws2  13442  lsws3  13443  lsws4  13444  wrdlen2i  13477  relexpsucnnr  13556  relexpaddg  13584  shftfib  13603  limsupcl  13995  limsupgf  13997  limsupval2  14002  isercolllem3  14188  modfsummods  14309  ackbijnn  14342  supcvg  14370  fprodfac  14485  fprodmodd  14510  fallfac0  14541  bpoly4  14572  ege2le3  14602  rpnnen2lem5  14729  ruclem11  14751  fsumdvds  14811  fproddvdsd  14840  mod2eq1n2dvds  14852  oddnn02np1  14853  oddge22np1  14854  evennn02n  14855  evennn2n  14856  bitsinv2  14946  sadaddlem  14969  smupf  14981  smup0  14982  smu01lem  14988  3lcm2e6woprm  15109  6lcm4e12  15110  lcmfunsnlem1  15131  lcmfunsnlem2lem1  15132  lcmfunsnlem2  15134  coprmprod  15156  isprm6  15207  hashdvds  15261  phisum  15276  reumodprminv  15290  prmreclem6  15406  vdwlem13  15478  ramtlecl  15485  0ram  15505  prmdvdsprmo  15527  fvprmselgcd1  15530  prmgaplcmlem1  15536  prmgaplem7  15542  prmgaplcm  15545  cshwshashnsame  15591  prmlem0  15593  wunndx  15654  prdsval  15881  xpsbas  16000  xpsadd  16002  xpsmul  16003  xpssca  16004  xpsvsca  16005  xpsless  16006  xpsle  16007  mreexexlem2d  16071  mreacs  16085  acsfn  16086  isofn  16201  ciclcl  16228  cicrcl  16229  cicsym  16230  cicer  16232  idfu2nd  16303  idfucl  16307  fucsect  16398  initoeu2lem1  16430  initoeu2lem2  16431  setccatid  16500  setcepi  16504  catchomfval  16514  estrccatid  16538  estrreslem1  16543  estrreslem2  16544  estrres  16545  funcestrcsetclem8  16553  fullestrcsetc  16557  embedsetcestrclem  16563  funcsetcestrclem8  16568  uncfval  16640  oduglb  16905  odumeet  16906  odulub  16907  odujoin  16908  isipodrs  16927  fpwipodrs  16930  isacs5lem  16935  idmhm  17110  submacs  17131  frmdup1  17167  mgmnsgrpex  17184  mulgneg2  17341  subgacs  17395  nsgacs  17396  idrespermg  17597  psgnunilem5  17680  psgnsn  17706  odf1o2  17754  frgpuplem  17951  cygctb  18059  gsumzunsnd  18121  gsum2dlem2  18136  gsummptnn0fz  18148  dprdsubg  18189  dmdprdsplit2lem  18210  dmdprdpr  18214  dprdpr  18215  dpjeq  18224  ablfac1eulem  18237  pgpfac1lem2  18240  pgpfaclem1  18246  srgbinomlem4  18309  unitgrp  18433  isirred  18465  brric  18510  mptscmfsupp0  18694  lssacs  18731  pwssplit1  18823  lbsextlem2  18923  lbsextlem3  18924  isnzr2hash  19028  0ring01eqbi  19037  rng1nnzr  19038  psrass1lem  19141  psrlidm  19167  resspsradd  19180  resspsrmul  19181  resspsrvsca  19182  mplcoe5lem  19231  ltbwe  19236  coe1fsupp  19348  psropprmul  19372  coe1add  19398  coe1mul2lem1  19401  coe1tm  19407  cply1coe0bi  19434  evls1rhmlem  19450  evl1sca  19462  evl1var  19464  pf1mpf  19480  pf1ind  19483  xrsmcmn  19531  xrs1mnd  19546  xrs10  19547  gsumfsum  19575  zringlpir  19597  zringcyg  19598  zndvds  19659  regsumsupp  19729  uvcvv1  19886  lsslinds  19928  matmulr  20002  ofco2  20015  mat0dimbas0  20030  mat1dimelbas  20035  mat1f1o  20042  dmatval  20056  scmatghm  20097  mavmul0  20116  mavmul0g  20117  m1detdiag  20161  mdetunilem9  20184  maducoeval2  20204  madugsum  20207  smadiadetlem0  20225  smadiadetlem1a  20227  smadiadetlem4  20233  smadiadetglem1  20235  smadiadetglem2  20236  smadiadetg  20237  cramer0  20254  cpmat  20272  mat2pmatfval  20286  cpm2mfval  20312  m2cpminvid2lem  20317  pmatcollpw3fi1lem2  20350  pmatcollpw3fi1  20351  idpm2idmp  20364  pm2mpmhmlem2  20382  chpmatfval  20393  chfacfscmulfsupp  20422  chfacfpmmulfsupp  20426  cpmidpmatlem2  20434  cpmadugsumlemF  20439  cpmidgsum2  20442  cpmadumatpolylem1  20444  cayhamlem3  20450  cayhamlem4  20451  indistopon  20554  mreclatdemoBAD  20649  mnfnei  20774  resthauslem  20916  sshauslem  20925  discmp  20950  conima  20977  1stcfb  20997  ptbasfi  21133  hauseqlcld  21198  xkoptsub  21206  xkofvcn  21236  idqtop  21258  tgqtop  21264  kqdisj  21284  xpstopnlem1  21361  xpstopnlem2  21363  ufildom1  21479  alexsubb  21599  alexsubALTlem3  21602  ptcmplem2  21606  ptcmplem3  21607  tmdgsum  21648  ustneism  21776  ustuqtop1  21794  iducn  21836  prdsmet  21923  imasdsf1olem  21926  xpsxmet  21933  xpsdsval  21934  xpsmet  21935  prdsbl  22044  met1stc  22074  prdsxmslem2  22082  xpsxms  22087  xpsms  22088  psmetutop  22120  dscmet  22125  nmoffn  22254  nmofval  22257  nmolb  22260  nmof  22262  cnbl0  22316  xrsmopn  22352  xrge0gsumle  22373  xrge0tsms  22374  negfcncf  22458  cnrehmeo  22488  lebnum  22499  xlebnum  22500  reparphti  22533  pcopt  22558  pcopt2  22559  pcorevcl  22561  pcorevlem  22562  pi1xfrval  22590  pi1xfrcnvlem  22592  pi1xfrcnv  22593  pi1cof  22595  pi1coval  22596  nmhmcn  22656  cphsubrglem  22706  csscld  22771  cmetcaulem  22809  cmpcmet  22838  ovolunlem1  22986  ovolicc2lem4  23009  ioovolcl  23058  ioorcl2  23060  uniioovol  23067  uniioombllem4  23074  uniioombllem5  23075  uniioombllem6  23076  dyadmbllem  23087  mbfsub  23149  itg1climres  23201  xrge0f  23218  itg2ge0  23222  itg2i1fseq2  23243  ibl0  23273  ellimc2  23361  limcflf  23365  dvreslem  23393  dvidlem  23399  dvid  23401  cpnres  23420  dvaddbr  23421  dvmulbr  23422  dvfre  23434  dvexp  23436  dvrec  23438  dvmptid  23440  dvmptc  23441  dvmptntr  23454  dvexp3  23459  dvlipcn  23475  dveq0  23481  dv11cn  23482  lhop2  23496  ftc1a  23518  tdeglem1  23536  tdeglem3  23537  tdeglem4  23538  tdeglem2  23539  mdeg0  23548  mdegle0  23555  ply1remlem  23640  plypf1  23686  coe0  23730  dvply1  23757  elqaalem3  23794  aaliou2b  23814  aaliou3lem8  23818  aaliou3lem7  23822  taylfvallem  23830  taylf  23833  tayl0  23834  taylpfval  23837  taylply  23841  dvtaylp  23842  taylthlem1  23845  taylthlem2  23846  ulmdvlem1  23872  ulmdvlem2  23873  ulmdvlem3  23874  radcnvcl  23889  psercnlem2  23896  psercn  23898  pserdv  23901  abelthlem3  23905  abelth  23913  sincn  23916  coscn  23917  reefgim  23922  tangtx  23975  pige3  23987  cosordlem  23995  logcn  24107  dvlog  24111  advlog  24114  advlogexp  24115  logtayl  24120  logccv  24123  dvcxp1  24195  dvcncxp1  24198  cxpcn3lem  24202  cxpcn3  24203  resqrtcn  24204  sqrtcn  24205  loglesqrt  24213  logbfval  24242  logblog  24244  isosctrlem2  24263  dquartlem1  24292  quart  24302  atancj  24351  efiatan  24353  atantan  24364  atanbndlem  24366  atansopn  24373  dvatan  24376  atantayl  24378  leibpilem2  24382  leibpi  24383  log2tlbnd  24386  rlimcnp2  24407  efrlim  24410  divsqrtsumlem  24420  jensenlem1  24427  jensenlem2  24428  jensen  24429  amgmlem  24430  amgm  24431  emcllem4  24439  emcllem7  24442  lgamcvg2  24495  gamcvg2lem  24499  wilthlem2  24509  wilthlem3  24510  basellem6  24526  chtrpcl  24615  ppiltx  24617  1sgm2ppw  24639  chtlepsi  24645  chpub  24659  logfacbnd3  24662  logfacrlim  24663  perfectlem2  24669  dchrelbas2  24676  dchrabs  24699  dchrhash  24710  bposlem7  24729  lgsdir2lem5  24768  lgsqrlem1  24785  gausslemma2dlem5  24810  gausslemma2dlem6  24811  lgseisenlem4  24817  lgsquad2lem1  24823  lgsquad3  24826  chpo1ub  24883  vmadivsumb  24886  rpvmasumlem  24890  dchrisumlem2  24893  dchrmusumlema  24896  dchrvmasumlem2  24901  dchrvmasumlema  24903  dchrvmasumiflem1  24904  dchrisum0flblem1  24911  dchrisum0lem1  24919  rplogsum  24930  mudivsum  24933  logdivsum  24936  mulog2sumlem2  24938  vmalogdivsum2  24941  2vmadivsumlem  24943  log2sumbnd  24947  selberglem2  24949  selbergb  24952  selberg2lem  24953  selberg2b  24955  selberg3lem1  24960  selberg4lem1  24963  selberg4  24964  pntrsumo1  24968  pntrlog2bndlem2  24981  pntrlog2bndlem3  24982  pntrlog2bndlem4  24983  pntrlog2bndlem5  24984  pntibndlem1  24992  pntibndlem2  24994  pntibndlem3  24995  pntlemb  25000  pntlemr  25005  pntlemf  25008  pntlem3  25012  pnt  25017  qabvle  25028  padicabv  25033  ostth1  25036  istrkg2ld  25073  tgldimor  25111  tgcgr4  25141  motgrp  25153  perpln1  25320  perpln2  25321  isperp  25322  uhgrares  25600  umgrares  25616  edgopval  25632  usgrares  25661  nbgraop  25715  nbgraopALT  25716  nbgraf1o0  25738  cusgra0v  25752  cusgra1v  25753  cusgraexilem2  25759  sizeusglecusg  25777  isuvtx  25779  2trllemH  25845  wlkntrllem3  25854  2wlklem1  25890  usgra2wlkspthlem1  25910  usgra2wlkspthlem2  25911  constr3trllem3  25943  constr3pthlem3  25948  wwlkn  25973  wlkiswwlk2  25988  wwlkn0s  25996  usg2wlkeq  25999  wlknwwlknvbij  26031  clwwlkn  26058  clwwlkn2  26066  clwlkisclwwlklem2  26077  clwwlkvbij  26092  hashecclwwlkn1  26124  usghashecclwwlk  26125  vdgr0  26190  rusgrasn  26235  eupatrl  26258  eupares  26265  vdegp1ai  26274  vdegp1bi  26275  frgra3v  26292  frgrancvvdeqlem9  26331  frgrancvvdgeq  26333  frg2wot1  26347  usgreghash2spotv  26356  extwwlkfablem2  26368  numclwwlkovf2  26374  ex-lcm  26470  vsfval  26655  ipasslem7  26878  minvecolem2  26918  h2hcau  27023  h2hlm  27024  hlimadd  27237  hhsscms  27323  chocunii  27347  occllem  27349  leopnmid  28184  opsqrlem1  28186  hmopidmchi  28197  mdslj1i  28365  addltmulALT  28492  imadifxp  28599  xaddeq0  28710  xrge0npcan  28828  gsumle  28913  xrge0tsmsd  28919  locfinreflem  29038  locfinref  29039  xpinpreima2  29084  cnre2csqlem  29087  tpr2rico  29089  ordtrestNEW  29098  ordtrest2NEW  29100  mndpluscn  29103  pnfneige0  29128  qqhghm  29163  qqhrhm  29164  qqhcn  29166  qqhucn  29167  rrhcn  29172  rrhre  29196  esumsplit  29245  esumpr  29258  esumfsup  29262  sigaclcu2  29313  pwsiga  29323  prsiga  29324  sigapildsys  29355  ldgenpisyslem1  29356  measvuni  29407  elmbfmvol2  29459  mbfmcnt  29460  sxbrsigalem1  29477  sxbrsiga  29482  omsfval  29486  carsgclctunlem2  29511  sibf0  29526  sitgclg  29534  sitmval  29541  eulerpartgbij  29564  eulerpartlemgh  29570  isrrvv  29635  rrvadd  29644  rrvmulc  29645  dstrvprob  29663  coinflipspace  29672  coinfliprv  29674  ballotlemfmpn  29686  ballotlem1ri  29726  sgnmulsgn  29741  plymul02  29752  signsplypnf  29756  signsply0  29757  signswrid  29764  indispcon  30273  conpcon  30274  iccllyscon  30289  cvmopnlem  30317  cvmliftlem15  30337  cvmlift2lem3  30344  mrsubff  30466  mrsubccat  30472  circum  30625  elhf2  31255  topdifinfindis  32170  icoreelrn  32185  finxpreclem2  32203  finixpnum  32364  matunitlindflem1  32375  matunitlindflem2  32376  poimirlem5  32384  poimirlem10  32389  poimirlem22  32401  poimirlem26  32405  poimirlem27  32406  poimirlem28  32407  poimirlem29  32408  poimirlem31  32410  poimirlem32  32411  mblfinlem3  32418  mblfinlem4  32419  ismblfin  32420  ovoliunnfl  32421  voliunnfl  32423  volsupnfl  32424  dvtan  32430  itg2addnclem  32431  ftc1anclem5  32459  dvasin  32466  dvreasin  32468  dvreacos  32469  areacirclem1  32470  areacirc  32475  bnd2lem  32560  prdsbnd  32562  cntotbnd  32565  cnpwstotbnd  32566  isdrngo2  32727  prter2  32984  eqlkr2  33205  tendoidcl  34875  cdlemk56  35077  dihpN  35443  mapdhval  35831  hlhillcs  36068  isnacs3  36091  diophrw  36140  lzenom  36151  diophin  36154  pellexlem5  36215  pw2f1ocnv  36422  dnnumch2  36433  kelac2lem  36452  kelac2  36453  dfac21  36454  pwfi2f1o  36484  frlmpwfi  36486  mpaaeu  36539  rngunsnply  36562  mendbas  36573  mendplusgfval  36574  mendmulrfval  36576  mendsca  36578  mendvscafval  36579  subrgacs  36589  sdrgacs  36590  cntzsdrg  36591  idomodle  36593  proot1ex  36598  deg1mhm  36604  itgpowd  36619  trclubgNEW  36744  dmtrcl  36753  rntrcl  36754  brfvidRP  36799  trclrelexplem  36822  relexp01min  36824  trclimalb2  36837  dssmapfvd  37131  ntrk0kbimka  37157  ntrrn  37240  dssmapntrcls  37246  amgm2d  37323  amgm3d  37324  amgm4d  37325  hashnzfzclim  37343  ofsubid  37345  ofdivrec  37347  dvconstbi  37355  fzisoeu  38255  iuneqfzuzlem  38292  sumnnodd  38498  negcncfg  38567  cnfdmsn  38568  divcncf  38570  dvmptresicc  38610  itgcoscmulx  38662  stoweidlem13  38707  stoweidlem26  38720  stoweidlem34  38728  stoweidlem42  38736  stoweidlem44  38738  stoweidlem48  38742  stoweidlem62  38756  stoweid  38757  stirlinglem7  38774  stirlinglem11  38778  stirlinglem12  38779  dirkeritg  38796  dirkercncflem2  38798  dirkercncflem4  38800  fourierdlem16  38817  fourierdlem21  38822  fourierdlem22  38823  fourierdlem24  38825  fourierdlem48  38848  fourierdlem49  38849  fourierdlem62  38862  fourierdlem70  38870  fourierdlem80  38880  fourierdlem83  38883  fourierdlem85  38885  fourierdlem102  38902  fourierdlem104  38904  fourierdlem111  38911  fourierdlem112  38912  fourierdlem114  38914  etransclem18  38946  etransclem23  38951  etransclem24  38952  etransclem25  38953  etransclem35  38963  etransclem46  38974  ovolval5lem3  39345  iccpartipre  39761  iccpartiltu  39762  fmtnoprmfac2lem1  39818  mod42tp1mod8  39859  sfprmdvdsmersenne  39860  perfectALTVlem2  39967  stgoldbwt  40000  nnsum3primesgbe  40010  nnsum4primesodd  40014  nnsum4primesoddALTV  40015  nnsum4primeseven  40018  nnsum4primesevenALTV  40019  bgoldbtbndlem2  40024  mptmpt2opabbrd  40159  snstrvtxval  40267  snstriedgval  40268  isuhgrop  40294  uhgrunop  40299  uhgrstrrepe  40303  edgastruct  40355  isusgrs  40385  isusgrop  40391  usgrop  40392  uspgr1ewop  40473  usgr2v1e2w  40477  uhgrspan1  40526  upgrres1  40531  umgrres1  40532  usgrres1  40533  isfusgrcl  40539  fusgredgfi  40543  usgr1v0e  40544  nbgrval  40559  nbusgrf1o1  40597  nbfusgrlevtxm2  40605  uvtxa01vtx0  40622  nbupgruvtxres  40633  usgrexi  40660  cusgrexi  40661  cusgrres  40663  cusgrfilem3  40672  sizusglecusg  40678  vtxdgfval  40682  vtxdgf  40685  vtxdlfgrval  40699  vtxd0nedgb  40702  vtxdusgr0edgnelALT  40710  1loopgrvd0  40718  1egrvtxdg1  40724  1egrvtxdg0  40726  p1evtxdeqlem  40727  p1evtxdeq  40728  p1evtxdp1  40729  umgr2v2eedg  40739  umgr2v2e  40740  vdiscusgrb  40745  vdegp1ai-av  40751  vdegp1bi-av  40752  ewlkle  40806  1wlksfval  40810  wlksfval  40811  1wlksv  40823  1wlk1ewlk  40843  uspgr2wlkeq  40853  1wlkp1lem8  40888  upgr2pthnlp  40937  1wlkiswwlks2  41071  wlksnwwlknvbij  41113  wwlksnextproplem1  41114  2pthdlem1  41136  elwwlks2  41169  clwlkclwwlklem1  41207  clwwlksnfi  41219  clwwlksvbij  41228  hashecclwwlksn1  41260  umgrhashecclwwlk  41261  0wlkOnlem1  41285  0wlkOns1  41288  31wlkdlem4  41328  upgr3v3e3cycl  41346  trlsegvdeglem3  41389  trlsegvdeglem5  41391  eupth2lemb  41404  frgr3v  41444  frgr2wwlk1  41493  fusgreghash2wspv  41498  idmgmhm  41577  mgmplusgiopALT  41619  sgrp2sgrp  41653  isrnghm  41681  lidlmmgm  41714  2zrngnmlid  41738  dfrngc2  41763  rnghmsscmap2  41764  rnghmsscmap  41765  rngchomfvalALTV  41775  rngcidALTV  41782  funcrngcsetcALT  41790  dfringc2  41809  rhmsscmap2  41810  rhmsscmap  41811  rhmsscrnghm  41817  rngcresringcat  41821  funcringcsetcALTV2lem8  41834  ringchomfvalALTV  41838  ringcidALTV  41845  funcringcsetclem8ALTV  41857  srhmsubc  41867  fldc  41874  rngcrescrhm  41876  rhmsubclem3  41879  srhmsubcALTV  41886  fldcALTV  41893  rngcrescrhmALTV  41895  altgsumbcALT  41923  zlmodzxzel  41925  zlmodzxzsubm  41929  zlmodzxzsub  41930  gsumpr  41931  scmsuppss  41946  ply1mulgsum  41971  dmatALTbas  41983  lcoop  41993  lincval0  41997  lco0  42009  linds0  42047  snlindsntorlem  42052  lmod1lem2  42070  lmod1lem3  42071  lmod1zr  42075  lmod1zrnlvec  42076  zlmodzxznm  42079  zlmodzxzldeplem4  42085  expnegico01  42101  pw2m1lepw2m1  42103  fldivexpfllog2  42156  blennnelnn  42167  blenpw2  42169  nnpw2pmod  42174  blennnt2  42180  nnolog2flm1  42181  digfval  42188  dignnld  42194  dig2nn0ld  42195  0dig2nn0e  42203  0dig2nn0o  42204  amgmwlem  42317  amgmlemALT  42318  amgmw2d  42319
  Copyright terms: Public domain W3C validator