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  5489  fvrnressn  6393  isomin  6552  isoini  6553  mptmpt2opabbrd  7208  supp0  7260  suppval1  7261  suppssr  7286  dmtpos  7324  mpt2curryd  7355  oaabs2  7685  elqsecl  7761  mapsncnv  7864  boxcutc  7911  domunsncan  8020  unxpdom2  8128  sucxpdom  8129  findcard2d  8162  ac6sfi  8164  xpfi  8191  imafi  8219  snopfsupp  8258  fifo  8298  ordtypelem4  8386  oismo  8405  wofib  8410  brwdom2  8438  canthwdom  8444  cantnfval  8525  cantnflt  8529  cantnff  8531  cantnf0  8532  cantnfp1lem1  8535  cantnfp1lem3  8537  cantnflem1b  8543  cantnflem1  8546  cnfcom  8557  cnfcom2lem  8558  ranksnb  8650  tskwe  8736  cardidm  8745  infxpenc  8801  fseqdom  8809  dfac8clem  8815  dfac12lem2  8926  infmap2  9000  isfin4-3  9097  fin23lem14  9115  fin23lem40  9133  isf34lem7  9161  isf34lem6  9162  fin1a2lem12  9193  hsmexlem4  9211  hsmexlem5  9212  ac5b  9260  alephexp1  9361  alephsuc3  9362  fpwwe2lem8  9419  fpwwe2lem13  9424  canthwe  9433  canthp1lem2  9435  gchcda1  9438  pwfseqlem5  9445  wunco  9515  prlem934  9815  supsrlem  9892  msqge0  10509  negfi  10931  ofnegsub  10978  ofsubge0  10979  xaddpnf1  12016  supxrmnf  12106  fz0sn0fz1  12413  injresinjlem  12544  fldiv4lem1div2  12594  uzindi  12737  seqfeq4  12806  seqof  12814  bcval5  13061  hashdomi  13125  hash1snb  13163  hashge2el2difr  13217  hashtpg  13221  fi1uzind  13234  fi1uzindOLD  13240  ccatlen  13315  lswccatn0lsw  13328  ccatalpha  13330  eqs1  13347  s111  13350  swrd0  13388  swrdspsleq  13403  wrdeqs1cat  13428  reps  13470  repsw0  13477  repswccat  13485  repswrevw  13486  lswcshw  13514  cshwsexa  13523  scshwfzeqfzo  13525  lsws2  13601  lsws3  13602  lsws4  13603  wrdlen2i  13636  relexpsucnnr  13715  relexpaddg  13743  shftfib  13762  limsupcl  14154  limsupgf  14156  limsupval2  14161  isercolllem3  14347  modfsummods  14471  ackbijnn  14504  supcvg  14532  fprodfac  14647  fprodmodd  14672  fallfac0  14703  bpoly4  14734  ege2le3  14764  rpnnen2lem5  14891  ruclem11  14913  fsumdvds  14973  fproddvdsd  15002  mod2eq1n2dvds  15014  oddnn02np1  15015  oddge22np1  15016  evennn02n  15017  evennn2n  15018  bitsinv2  15108  sadaddlem  15131  smupf  15143  smup0  15144  smu01lem  15150  3lcm2e6woprm  15271  6lcm4e12  15272  lcmfunsnlem1  15293  lcmfunsnlem2lem1  15294  lcmfunsnlem2  15296  coprmprod  15318  isprm6  15369  hashdvds  15423  phisum  15438  reumodprminv  15452  prmreclem6  15568  vdwlem13  15640  ramtlecl  15647  0ram  15667  prmdvdsprmo  15689  fvprmselgcd1  15692  prmgaplcmlem1  15698  prmgaplem7  15704  prmgaplcm  15707  cshwshashnsame  15753  prmlem0  15755  wunndx  15819  prdsval  16055  xpsbas  16174  xpsadd  16176  xpsmul  16177  xpssca  16178  xpsvsca  16179  xpsless  16180  xpsle  16181  mreexexlem2d  16245  mreacs  16259  acsfn  16260  isofn  16375  ciclcl  16402  cicrcl  16403  cicsym  16404  cicer  16406  idfu2nd  16477  idfucl  16481  fucsect  16572  initoeu2lem1  16604  initoeu2lem2  16605  setccatid  16674  setcepi  16678  catchomfval  16688  estrccatid  16712  estrreslem1  16717  estrreslem2  16718  estrres  16719  funcestrcsetclem8  16727  fullestrcsetc  16731  embedsetcestrclem  16737  funcsetcestrclem8  16742  uncfval  16814  oduglb  17079  odumeet  17080  odulub  17081  odujoin  17082  isipodrs  17101  fpwipodrs  17104  isacs5lem  17109  idmhm  17284  submacs  17305  frmdup1  17341  mgmnsgrpex  17358  mulgneg2  17515  subgacs  17569  nsgacs  17570  idrespermg  17771  psgnunilem5  17854  psgnsn  17880  odf1o2  17928  frgpuplem  18125  cygctb  18233  gsumzunsnd  18295  gsum2dlem2  18310  gsummptnn0fz  18322  dprdsubg  18363  dmdprdsplit2lem  18384  dmdprdpr  18388  dprdpr  18389  dpjeq  18398  ablfac1eulem  18411  pgpfac1lem2  18414  pgpfaclem1  18420  srgbinomlem4  18483  unitgrp  18607  isirred  18639  brric  18684  mptscmfsupp0  18868  lssacs  18907  pwssplit1  18999  lbsextlem2  19099  lbsextlem3  19100  isnzr2hash  19204  0ring01eqbi  19213  rng1nnzr  19214  psrass1lem  19317  psrlidm  19343  resspsradd  19356  resspsrmul  19357  resspsrvsca  19358  mplcoe5lem  19407  ltbwe  19412  coe1fsupp  19524  psropprmul  19548  coe1add  19574  coe1mul2lem1  19577  coe1tm  19583  cply1coe0bi  19610  evls1rhmlem  19626  evl1sca  19638  evl1var  19640  pf1mpf  19656  pf1ind  19659  xrsmcmn  19709  xrs1mnd  19724  xrs10  19725  gsumfsum  19753  zringlpir  19777  zringcyg  19779  zndvds  19838  regsumsupp  19908  uvcvv1  20068  lsslinds  20110  matmulr  20184  ofco2  20197  mat0dimbas0  20212  mat1dimelbas  20217  mat1f1o  20224  dmatval  20238  scmatghm  20279  mavmul0  20298  mavmul0g  20299  m1detdiag  20343  mdetunilem9  20366  maducoeval2  20386  madugsum  20389  smadiadetlem0  20407  smadiadetlem1a  20409  smadiadetlem4  20415  smadiadetglem1  20417  smadiadetglem2  20418  smadiadetg  20419  cramer0  20436  cpmat  20454  mat2pmatfval  20468  cpm2mfval  20494  m2cpminvid2lem  20499  pmatcollpw3fi1lem2  20532  pmatcollpw3fi1  20533  idpm2idmp  20546  pm2mpmhmlem2  20564  chpmatfval  20575  chfacfscmulfsupp  20604  chfacfpmmulfsupp  20608  cpmidpmatlem2  20616  cpmadugsumlemF  20621  cpmidgsum2  20624  cpmadumatpolylem1  20626  cayhamlem3  20632  cayhamlem4  20633  indistopon  20745  mreclatdemoBAD  20840  mnfnei  20965  resthauslem  21107  sshauslem  21116  discmp  21141  connima  21168  1stcfb  21188  ptbasfi  21324  hauseqlcld  21389  xkoptsub  21397  xkofvcn  21427  idqtop  21449  tgqtop  21455  kqdisj  21475  xpstopnlem1  21552  xpstopnlem2  21554  ufildom1  21670  alexsubb  21790  alexsubALTlem3  21793  ptcmplem2  21797  ptcmplem3  21798  tmdgsum  21839  ustneism  21967  ustuqtop1  21985  iducn  22027  prdsmet  22115  imasdsf1olem  22118  xpsxmet  22125  xpsdsval  22126  xpsmet  22127  prdsbl  22236  met1stc  22266  prdsxmslem2  22274  xpsxms  22279  xpsms  22280  psmetutop  22312  dscmet  22317  nmoffn  22455  nmofval  22458  nmolb  22461  nmof  22463  cnbl0  22517  xrsmopn  22555  xrge0gsumle  22576  xrge0tsms  22577  negfcncf  22662  cnrehmeo  22692  lebnum  22703  xlebnum  22704  reparphti  22737  pcopt  22762  pcopt2  22763  pcorevcl  22765  pcorevlem  22766  pi1xfrval  22794  pi1xfrcnvlem  22796  pi1xfrcnv  22797  pi1cof  22799  pi1coval  22800  nmhmcn  22860  cphsubrglem  22917  csscld  22988  cmetcaulem  23026  cmpcmet  23056  divcncf  23156  ovolunlem1  23205  ovolicc2lem4  23228  ioovolcl  23278  ioorcl2  23280  uniioovol  23287  uniioombllem4  23294  uniioombllem5  23295  uniioombllem6  23296  dyadmbllem  23307  mbfsub  23369  itg1climres  23421  xrge0f  23438  itg2ge0  23442  itg2i1fseq2  23463  ibl0  23493  ellimc2  23581  limcflf  23585  dvreslem  23613  dvidlem  23619  dvid  23621  cpnres  23640  dvaddbr  23641  dvmulbr  23642  dvfre  23654  dvexp  23656  dvrec  23658  dvmptid  23660  dvmptc  23661  dvmptntr  23674  dvexp3  23679  dvlipcn  23695  dveq0  23701  dv11cn  23702  lhop2  23716  ftc1a  23738  tdeglem1  23756  tdeglem3  23757  tdeglem4  23758  tdeglem2  23759  mdeg0  23768  mdegle0  23775  ply1remlem  23860  plypf1  23906  coe0  23950  dvply1  23977  elqaalem3  24014  aaliou2b  24034  aaliou3lem8  24038  aaliou3lem7  24042  taylfvallem  24050  taylf  24053  tayl0  24054  taylpfval  24057  taylply  24061  dvtaylp  24062  taylthlem1  24065  taylthlem2  24066  ulmdvlem1  24092  ulmdvlem2  24093  ulmdvlem3  24094  radcnvcl  24109  psercnlem2  24116  psercn  24118  pserdv  24121  abelthlem3  24125  abelth  24133  sincn  24136  coscn  24137  reefgim  24142  tangtx  24195  pige3  24207  cosordlem  24215  logcn  24327  dvlog  24331  advlog  24334  advlogexp  24335  logtayl  24340  logccv  24343  dvcxp1  24415  dvcncxp1  24418  cxpcn3lem  24422  cxpcn3  24423  resqrtcn  24424  sqrtcn  24425  loglesqrt  24433  logbfval  24462  logblog  24464  isosctrlem2  24483  dquartlem1  24512  quart  24522  atancj  24571  efiatan  24573  atantan  24584  atanbndlem  24586  atansopn  24593  dvatan  24596  atantayl  24598  leibpilem2  24602  leibpi  24603  log2tlbnd  24606  rlimcnp2  24627  efrlim  24630  divsqrtsumlem  24640  jensenlem1  24647  jensenlem2  24648  jensen  24649  amgmlem  24650  amgm  24651  emcllem4  24659  emcllem7  24662  lgamcvg2  24715  gamcvg2lem  24719  wilthlem2  24729  wilthlem3  24730  basellem6  24746  chtrpcl  24835  ppiltx  24837  1sgm2ppw  24859  chtlepsi  24865  chpub  24879  logfacbnd3  24882  logfacrlim  24883  perfectlem2  24889  dchrelbas2  24896  dchrabs  24919  dchrhash  24930  bposlem7  24949  lgsdir2lem5  24988  lgsqrlem1  25005  gausslemma2dlem5  25030  gausslemma2dlem6  25031  lgseisenlem4  25037  lgsquad2lem1  25043  lgsquad3  25046  chpo1ub  25103  vmadivsumb  25106  rpvmasumlem  25110  dchrisumlem2  25113  dchrmusumlema  25116  dchrvmasumlem2  25121  dchrvmasumlema  25123  dchrvmasumiflem1  25124  dchrisum0flblem1  25131  dchrisum0lem1  25139  rplogsum  25150  mudivsum  25153  logdivsum  25156  mulog2sumlem2  25158  vmalogdivsum2  25161  2vmadivsumlem  25163  log2sumbnd  25167  selberglem2  25169  selbergb  25172  selberg2lem  25173  selberg2b  25175  selberg3lem1  25180  selberg4lem1  25183  selberg4  25184  pntrsumo1  25188  pntrlog2bndlem2  25201  pntrlog2bndlem3  25202  pntrlog2bndlem4  25203  pntrlog2bndlem5  25204  pntibndlem1  25212  pntibndlem2  25214  pntibndlem3  25215  pntlemb  25220  pntlemr  25225  pntlemf  25228  pntlem3  25232  pnt  25237  qabvle  25248  padicabv  25253  ostth1  25256  istrkg2ld  25293  tgldimor  25331  tgcgr4  25360  motgrp  25372  perpln1  25539  perpln2  25540  isperp  25541  snstrvtxval  25863  snstriedgval  25864  edgstruct  25878  isuhgrop  25895  uhgrunop  25900  uhgrstrrepe  25903  upgrunop  25943  umgrunop  25945  isusgrs  25978  isuspgrop  25983  isusgrop  25984  usgrop  25985  usgrstrrepe  26054  uspgr1ewop  26067  usgr2v1e2w  26071  uhgrspan1  26122  upgrres1  26127  umgrres1  26128  usgrres1  26129  isfusgrcl  26135  fusgredgfi  26139  usgr1v0e  26140  nbgrval  26155  nbusgrf1o1  26193  nbfusgrlevtxm2  26201  uvtxa01vtx0  26218  nbupgruvtxres  26229  usgrexilem  26257  usgrexi  26258  cusgrexi  26260  structtousgr  26262  structtocusgr  26263  cusgrres  26265  cusgrfilem3  26274  sizusglecusg  26280  vtxdgfval  26284  vtxdgf  26287  vtxdlfgrval  26301  vtxd0nedgb  26304  vtxdusgr0edgnelALT  26312  1loopgrvd0  26320  1egrvtxdg1  26325  1egrvtxdg0  26327  p1evtxdeqlem  26328  p1evtxdeq  26329  p1evtxdp1  26330  umgr2v2eedg  26340  umgr2v2e  26341  vdiscusgrb  26346  vdegp1ai  26352  vdegp1bi  26353  ewlkle  26405  wksfval  26409  wksv  26419  wlk1ewlk  26439  uspgr2wlkeq  26445  wlkp1lem8  26480  upgr2pthnlp  26531  wlkiswwlks2  26664  wlksnwwlknvbij  26706  wwlksnextproplem1  26707  2pthdlem1  26729  elwwlks2  26762  clwlkclwwlklem1  26801  clwwlksnfi  26813  clwwlksvbij  26822  hashecclwwlksn1  26854  umgrhashecclwwlk  26855  0wlkonlem1  26879  0wlkons1  26882  0pthon  26888  3wlkdlem4  26922  upgr3v3e3cycl  26940  trlsegvdeglem3  26982  trlsegvdeglem5  26984  eupth2lemb  26997  frgr3v  27037  frgr2wwlk1  27086  fusgreghash2wspv  27091  ex-lcm  27203  vsfval  27376  ipasslem7  27579  minvecolem2  27619  h2hcau  27724  h2hlm  27725  hlimadd  27938  hhsscms  28024  chocunii  28048  occllem  28050  leopnmid  28885  opsqrlem1  28887  hmopidmchi  28898  mdslj1i  29066  addltmulALT  29193  imadifxp  29300  xaddeq0  29402  fzodif2  29435  xrge0npcan  29521  gsumle  29606  xrge0tsmsd  29612  locfinreflem  29731  locfinref  29732  xpinpreima2  29777  cnre2csqlem  29780  tpr2rico  29782  ordtrestNEW  29791  ordtrest2NEW  29793  mndpluscn  29796  pnfneige0  29821  qqhghm  29856  qqhrhm  29857  qqhcn  29859  qqhucn  29860  rrhcn  29865  rrhre  29889  esumsplit  29938  esumpr  29951  esumfsup  29955  sigaclcu2  30006  pwsiga  30016  prsiga  30017  sigapildsys  30048  ldgenpisyslem1  30049  measvuni  30100  elmbfmvol2  30152  mbfmcnt  30153  sxbrsigalem1  30170  sxbrsiga  30175  omsfval  30179  carsgclctunlem2  30204  sibf0  30219  sitgclg  30227  sitmval  30234  eulerpartgbij  30257  eulerpartlemgh  30263  isrrvv  30328  rrvadd  30337  rrvmulc  30338  dstrvprob  30356  coinflipspace  30365  coinfliprv  30367  ballotlemfmpn  30379  ballotlem1ri  30419  sgnmulsgn  30434  plymul02  30445  signsplypnf  30449  signsply0  30450  signswrid  30457  itgexpif  30493  indispconn  30977  connpconn  30978  iccllysconn  30993  cvmopnlem  31021  cvmliftlem15  31041  cvmlift2lem3  31048  mrsubff  31170  mrsubccat  31176  circum  31329  noextend  31577  elhf2  31977  topdifinfindis  32865  icoreelrn  32880  finxpreclem2  32898  finixpnum  33065  matunitlindflem1  33076  matunitlindflem2  33077  poimirlem5  33085  poimirlem10  33090  poimirlem22  33102  poimirlem26  33106  poimirlem27  33107  poimirlem28  33108  poimirlem29  33109  poimirlem31  33111  poimirlem32  33112  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  dvtan  33131  itg2addnclem  33132  ftc1anclem5  33160  dvasin  33167  dvreasin  33169  dvreacos  33170  areacirclem1  33171  areacirc  33176  bnd2lem  33261  prdsbnd  33263  cntotbnd  33266  cnpwstotbnd  33267  isdrngo2  33428  prter2  33685  eqlkr2  33906  tendoidcl  35576  cdlemk56  35778  dihpN  36144  mapdhval  36532  hlhillcs  36769  isnacs3  36792  diophrw  36841  lzenom  36852  diophin  36855  pellexlem5  36916  pw2f1ocnv  37123  dnnumch2  37134  kelac2lem  37153  kelac2  37154  dfac21  37155  pwfi2f1o  37185  frlmpwfi  37187  mpaaeu  37240  rngunsnply  37263  mendbas  37274  mendplusgfval  37275  mendmulrfval  37277  mendsca  37279  mendvscafval  37280  subrgacs  37290  sdrgacs  37291  cntzsdrg  37292  idomodle  37294  proot1ex  37299  deg1mhm  37305  itgpowd  37320  trclubgNEW  37445  dmtrcl  37454  rntrcl  37455  brfvidRP  37500  trclrelexplem  37523  relexp01min  37525  trclimalb2  37538  dssmapfvd  37832  ntrk0kbimka  37858  ntrrn  37941  dssmapntrcls  37947  amgm2d  38022  amgm3d  38023  amgm4d  38024  hashnzfzclim  38042  ofsubid  38044  ofdivrec  38046  dvconstbi  38054  fzisoeu  39013  iuneqfzuzlem  39049  sumnnodd  39298  negcncfg  39429  cnfdmsn  39430  dvmptresicc  39471  itgcoscmulx  39522  stoweidlem13  39567  stoweidlem26  39580  stoweidlem34  39588  stoweidlem42  39596  stoweidlem44  39598  stoweidlem48  39602  stoweidlem62  39616  stoweid  39617  stirlinglem7  39634  stirlinglem11  39638  stirlinglem12  39639  dirkeritg  39656  dirkercncflem2  39658  dirkercncflem4  39660  fourierdlem16  39677  fourierdlem21  39682  fourierdlem22  39683  fourierdlem24  39685  fourierdlem48  39708  fourierdlem49  39709  fourierdlem62  39722  fourierdlem70  39730  fourierdlem80  39740  fourierdlem83  39743  fourierdlem85  39745  fourierdlem102  39762  fourierdlem104  39764  fourierdlem111  39771  fourierdlem112  39772  fourierdlem114  39774  etransclem18  39806  etransclem23  39811  etransclem24  39812  etransclem25  39813  etransclem35  39823  etransclem46  39834  ovolval5lem3  40205  setsidel  40674  iccpartipre  40685  iccpartiltu  40686  fmtnoprmfac2lem1  40807  mod42tp1mod8  40848  sfprmdvdsmersenne  40849  perfectALTVlem2  40956  stgoldbwt  40989  nnsum3primesgbe  40999  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbtbndlem2  41013  upwlksfval  41034  sprval  41047  sprbisymrel  41067  uspgrbisymrelALT  41081  idmgmhm  41106  mgmplusgiopALT  41148  sgrp2sgrp  41182  isrnghm  41210  lidlmmgm  41243  2zrngnmlid  41267  dfrngc2  41290  rnghmsscmap2  41291  rnghmsscmap  41292  rngchomfvalALTV  41302  rngcidALTV  41309  funcrngcsetcALT  41317  dfringc2  41336  rhmsscmap2  41337  rhmsscmap  41338  rhmsscrnghm  41344  rngcresringcat  41348  funcringcsetcALTV2lem8  41361  ringchomfvalALTV  41365  ringcidALTV  41372  funcringcsetclem8ALTV  41384  srhmsubc  41394  fldc  41401  rngcrescrhm  41403  rhmsubclem3  41406  srhmsubcALTV  41412  fldcALTV  41419  rngcrescrhmALTV  41421  altgsumbcALT  41449  zlmodzxzel  41451  zlmodzxzsubm  41455  zlmodzxzsub  41456  gsumpr  41457  scmsuppss  41471  ply1mulgsum  41496  dmatALTbas  41508  lcoop  41518  lincval0  41522  lco0  41534  linds0  41572  snlindsntorlem  41577  lmod1lem2  41595  lmod1lem3  41596  lmod1zr  41600  lmod1zrnlvec  41601  zlmodzxznm  41604  zlmodzxzldeplem4  41610  expnegico01  41626  pw2m1lepw2m1  41628  fldivexpfllog2  41681  blennnelnn  41692  blenpw2  41694  nnpw2pmod  41699  blennnt2  41705  nnolog2flm1  41706  digfval  41713  dignnld  41719  dig2nn0ld  41720  0dig2nn0e  41728  0dig2nn0o  41729  amgmwlem  41881  amgmlemALT  41882  amgmw2d  41883
  Copyright terms: Public domain W3C validator