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  5433  poirr2  5738  fvrnressn  6655  isomin  6814  isoini  6815  mptmpt2opabbrd  7484  supp0  7537  suppval1  7538  suppssr  7564  dmtpos  7602  mpt2curryd  7633  oaabs2  7965  elqsecl  8039  mapsncnv  8144  boxcutc  8191  domunsncan  8302  unxpdom2  8410  sucxpdom  8411  findcard2d  8444  ac6sfi  8446  xpfi  8473  imafi  8501  snopfsupp  8540  fifo  8580  ordtypelem4  8668  oismo  8687  wofib  8692  brwdom2  8720  canthwdom  8726  cantnfval  8815  cantnflt  8819  cantnff  8821  cantnf0  8822  cantnfp1lem1  8825  cantnfp1lem3  8827  cantnflem1b  8833  cantnflem1  8836  cnfcom  8847  cnfcom2lem  8848  ranksnb  8940  updjudhcoinlf  9044  updjudhcoinrg  9045  updjud  9046  tskwe  9062  cardidm  9071  infxpenc  9127  fseqdom  9135  dfac8clem  9141  dfac12lem2  9254  infmap2  9328  isfin4-3  9425  fin23lem14  9443  fin23lem40  9461  isf34lem7  9489  isf34lem6  9490  fin1a2lem12  9521  hsmexlem4  9539  hsmexlem5  9540  ac5b  9588  alephexp1  9689  alephsuc3  9690  fpwwe2lem8  9747  fpwwe2lem13  9752  canthwe  9761  canthp1lem2  9763  gchcda1  9766  pwfseqlem5  9773  wunco  9843  prlem934  10143  supsrlem  10220  msqge0  10837  negfi  11259  ofnegsub  11306  ofsubge0  11307  xaddpnf1  12278  supxrmnf  12368  fz0sn0fz1  12683  injresinjlem  12815  fldiv4lem1div2  12865  uzindi  13008  seqfeq4  13076  seqof  13084  bcval5  13328  hashdomi  13390  hash1snb  13427  hashge2el2difr  13483  hashtpg  13487  fi1uzind  13499  ccatlen  13575  lswccatn0lsw  13591  ccatalpha  13593  eqs1  13610  s111  13613  swrd0  13661  swrdspsleq  13676  wrdeqs1cat  13701  reps  13744  repsw0  13751  repswccat  13759  repswrevw  13760  lswcshw  13788  cshwsexa  13797  scshwfzeqfzo  13799  lsws2  13876  lsws3  13877  lsws4  13878  wrdlen2i  13914  relexpsucnnr  13991  relexpaddg  14019  shftfib  14038  limsupcl  14430  limsupgf  14432  limsupval2  14437  isercolllem3  14623  modfsummods  14750  ackbijnn  14785  supcvg  14813  fprodfac  14927  fprodmodd  14951  fallfac0  14982  bpoly4  15013  ege2le3  15043  rpnnen2lem5  15170  ruclem11  15192  fsumdvds  15256  fproddvdsd  15282  mod2eq1n2dvds  15294  oddnn02np1  15295  oddge22np1  15296  evennn02n  15297  evennn2n  15298  bitsinv2  15387  sadaddlem  15410  smupf  15422  smup0  15423  smu01lem  15429  3lcm2e6woprm  15550  6lcm4e12  15551  lcmfunsnlem1  15572  lcmfunsnlem2lem1  15573  lcmfunsnlem2  15575  coprmprod  15596  isprm6  15646  hashdvds  15700  phisum  15715  reumodprminv  15729  prmreclem6  15845  vdwlem13  15917  ramtlecl  15924  0ram  15944  prmdvdsprmo  15966  fvprmselgcd1  15969  prmgaplcmlem1  15975  prmgaplem7  15981  prmgaplcm  15984  cshwshashnsame  16025  prmlem0  16027  wunndx  16092  prdsval  16323  xpsbas  16442  xpsadd  16444  xpsmul  16445  xpssca  16446  xpsvsca  16447  xpsless  16448  xpsle  16449  mreexexlem2d  16513  mreacs  16526  acsfn  16527  isofn  16642  ciclcl  16669  cicrcl  16670  cicsym  16671  cicer  16673  idfu2nd  16744  idfucl  16748  fucsect  16839  initoeu2lem1  16871  initoeu2lem2  16872  setccatid  16941  setcepi  16945  catchomfval  16955  estrccatid  16979  estrreslem1  16984  estrreslem2  16985  estrresOLD  16986  estrres  16987  funcestrcsetclem8  16995  fullestrcsetc  16999  embedsetcestrclem  17005  funcsetcestrclem8  17010  uncfval  17082  oduglb  17347  odumeet  17348  odulub  17349  odujoin  17350  isipodrs  17369  fpwipodrs  17372  isacs5lem  17377  idmhm  17552  submacs  17573  frmdup1  17609  mgmnsgrpex  17626  mulgneg2  17781  subgacs  17834  nsgacs  17835  idrespermg  18035  psgnunilem5  18118  psgnsn  18144  odf1o2  18192  frgpuplem  18389  cygctb  18497  gsumzunsnd  18559  gsum2dlem2  18574  gsummptnn0fz  18586  gsummptnn0fzOLD  18587  dprdsubg  18628  dmdprdsplit2lem  18649  dmdprdpr  18653  dprdpr  18654  dpjeq  18663  ablfac1eulem  18676  pgpfac1lem2  18679  pgpfaclem1  18685  srgbinomlem4  18748  unitgrp  18872  isirred  18904  brric  18951  mptscmfsupp0  19135  lssacs  19177  pwssplit1  19269  lbsextlem2  19371  lbsextlem3  19372  isnzr2hash  19476  0ring01eqbi  19485  rng1nnzr  19486  psrass1lem  19589  psrlidm  19615  resspsradd  19628  resspsrmul  19629  resspsrvsca  19630  mplcoe5lem  19679  ltbwe  19684  coe1fsupp  19795  psropprmul  19819  coe1add  19845  coe1mul2lem1  19848  coe1tm  19854  cply1coe0bi  19881  evls1rhmlem  19897  evl1sca  19909  evl1var  19911  pf1mpf  19927  pf1ind  19930  xrsmcmn  19980  xrs1mnd  19995  xrs10  19996  gsumfsum  20024  zringlpir  20048  zringcyg  20050  zndvds  20108  regsumsupp  20180  uvcvv1  20342  lsslinds  20384  matmulr  20458  ofco2  20472  mat0dimbas0  20487  mat1dimelbas  20492  mat1f1o  20499  dmatval  20513  scmatghm  20554  mavmul0  20573  mavmul0g  20574  m1detdiag  20618  mdetunilem9  20641  maducoeval2  20661  madugsum  20664  smadiadetlem0  20683  smadiadetlem1a  20685  smadiadetlem4  20691  smadiadetglem1  20693  smadiadetglem2  20694  smadiadetg  20695  cramer0  20713  cpmat  20731  mat2pmatfval  20745  cpm2mfval  20771  m2cpminvid2lem  20776  pmatcollpw3fi1lem2  20809  pmatcollpw3fi1  20810  idpm2idmp  20823  pm2mpmhmlem2  20841  chpmatfval  20852  chfacfscmulfsupp  20881  chfacfpmmulfsupp  20885  cpmidpmatlem2  20893  cpmadugsumlemF  20898  cpmidgsum2  20901  cpmadumatpolylem1  20903  cayhamlem3  20909  cayhamlem4  20910  indistopon  21023  mreclatdemoBAD  21118  mnfnei  21243  resthauslem  21385  sshauslem  21394  discmp  21419  connima  21446  1stcfb  21466  ptbasfi  21602  hauseqlcld  21667  xkoptsub  21675  xkofvcn  21705  idqtop  21727  tgqtop  21733  kqdisj  21753  xpstopnlem1  21830  xpstopnlem2  21832  ufildom1  21947  alexsubb  22067  alexsubALTlem3  22070  ptcmplem2  22074  ptcmplem3  22075  tmdgsum  22116  ustneism  22244  ustuqtop1  22262  iducn  22304  prdsmet  22392  imasdsf1olem  22395  xpsxmet  22402  xpsdsval  22403  xpsmet  22404  prdsbl  22513  met1stc  22543  prdsxmslem2  22551  xpsxms  22556  xpsms  22557  psmetutop  22589  dscmet  22594  nmoffn  22732  nmofval  22735  nmolb  22738  nmof  22740  cnbl0  22794  xrsmopn  22832  xrge0gsumle  22853  xrge0tsms  22854  negfcncf  22939  cnrehmeo  22969  lebnum  22980  xlebnum  22981  reparphti  23013  pcopt  23038  pcopt2  23039  pcorevcl  23041  pcorevlem  23042  pi1xfrval  23070  pi1xfrcnvlem  23072  pi1xfrcnv  23073  pi1cof  23075  pi1coval  23076  nmhmcn  23136  cphsubrglem  23193  csscld  23264  cmetcaulem  23303  cmpcmet  23333  divcncf  23434  ovolunlem1  23484  ovolicc2lem4  23507  ioovolcl  23557  ioorcl2  23559  uniioovol  23566  uniioombllem4  23573  uniioombllem5  23574  uniioombllem6  23575  dyadmbllem  23586  mbfsub  23649  itg1climres  23701  xrge0f  23718  itg2ge0  23722  itg2i1fseq2  23743  ibl0  23773  ellimc2  23861  limcflf  23865  dvreslem  23893  dvidlem  23899  dvid  23901  cpnres  23920  dvaddbr  23921  dvmulbr  23922  dvfre  23934  dvexp  23936  dvrec  23938  dvmptid  23940  dvmptc  23941  dvmptntr  23954  dvexp3  23961  dvlipcn  23977  dveq0  23983  dv11cn  23984  lhop2  23998  ftc1a  24020  tdeglem1  24038  tdeglem3  24039  tdeglem4  24040  tdeglem2  24041  mdeg0  24050  mdegle0  24057  ply1remlem  24142  plypf1  24188  coe0  24232  dvply1  24259  elqaalem3  24296  aaliou2b  24316  aaliou3lem8  24320  aaliou3lem7  24324  taylfvallem  24332  taylf  24335  tayl0  24336  taylpfval  24339  taylply  24343  dvtaylp  24344  taylthlem1  24347  taylthlem2  24348  ulmdvlem1  24374  ulmdvlem2  24375  ulmdvlem3  24376  radcnvcl  24391  psercnlem2  24398  psercn  24400  pserdv  24403  abelthlem3  24407  abelth  24415  sincn  24418  coscn  24419  reefgim  24424  tangtx  24478  pige3  24490  cosordlem  24498  logcn  24613  dvlog  24617  advlog  24620  advlogexp  24621  logtayl  24626  logccv  24629  dvcxp1  24701  dvcncxp1  24704  cxpcn3lem  24708  cxpcn3  24709  resqrtcn  24710  sqrtcn  24711  loglesqrt  24719  logbfval  24748  logblog  24750  isosctrlem2  24769  dquartlem1  24798  quart  24808  atancj  24857  efiatan  24859  atantan  24870  atanbndlem  24872  atansopn  24879  dvatan  24882  atantayl  24884  leibpilem2  24888  leibpi  24889  log2tlbnd  24892  rlimcnp2  24913  efrlim  24916  divsqrtsumlem  24926  jensenlem1  24933  jensenlem2  24934  jensen  24935  amgmlem  24936  amgm  24937  emcllem4  24945  emcllem7  24948  lgamcvg2  25001  gamcvg2lem  25005  wilthlem2  25015  wilthlem3  25016  basellem6  25032  chtrpcl  25121  ppiltx  25123  1sgm2ppw  25145  chtlepsi  25151  chpub  25165  logfacbnd3  25168  logfacrlim  25169  perfectlem2  25175  dchrelbas2  25182  dchrabs  25205  dchrhash  25216  bposlem7  25235  lgsdir2lem5  25274  lgsqrlem1  25291  gausslemma2dlem5  25316  gausslemma2dlem6  25317  lgseisenlem4  25323  lgsquad2lem1  25329  lgsquad3  25332  chpo1ub  25389  vmadivsumb  25392  rpvmasumlem  25396  dchrisumlem2  25399  dchrmusumlema  25402  dchrvmasumlem2  25407  dchrvmasumlema  25409  dchrvmasumiflem1  25410  dchrisum0flblem1  25417  dchrisum0lem1  25425  rplogsum  25436  mudivsum  25439  logdivsum  25442  mulog2sumlem2  25444  vmalogdivsum2  25447  2vmadivsumlem  25449  log2sumbnd  25453  selberglem2  25455  selbergb  25458  selberg2lem  25459  selberg2b  25461  selberg3lem1  25466  selberg4lem1  25469  selberg4  25470  pntrsumo1  25474  pntrlog2bndlem2  25487  pntrlog2bndlem3  25488  pntrlog2bndlem4  25489  pntrlog2bndlem5  25490  pntibndlem1  25498  pntibndlem2  25500  pntibndlem3  25501  pntlemb  25506  pntlemr  25511  pntlemf  25514  pntlem3  25518  pnt  25523  qabvle  25534  padicabv  25539  ostth1  25542  istrkg2ld  25579  tgldimor  25617  tgcgr4  25646  motgrp  25658  perpln1  25825  perpln2  25826  isperp  25827  snstrvtxval  26149  snstriedgval  26150  isuhgrop  26185  uhgrunop  26190  uhgrstrrepe  26193  upgrop  26209  upgrunop  26234  umgrunop  26236  isusgrs  26272  isuspgrop  26277  isusgrop  26278  usgrop  26279  usgrstrrepe  26349  uspgr1ewop  26362  usgr2v1e2w  26366  uhgrspan1  26417  upgrres  26420  umgrres  26421  usgrres  26422  upgrres1  26427  umgrres1  26428  usgrres1  26429  isfusgrcl  26435  fusgredgfi  26439  usgr1v0e  26440  nbgrval  26451  nbusgrf1o1  26494  nbfusgrlevtxm2  26502  uvtx01vtx  26524  uvtxa01vtx0OLD  26526  usgrexilem  26570  usgrexi  26571  cusgrexi  26573  structtousgr  26575  structtocusgr  26576  cusgrres  26578  cusgrfilem3  26587  sizusglecusg  26593  vtxdgfval  26597  vtxdgop  26600  vtxdgf  26601  vtxdlfgrval  26615  vtxd0nedgb  26618  vtxdusgr0edgnelALT  26626  1loopgrvd0  26634  1egrvtxdg1  26639  1egrvtxdg0  26641  p1evtxdeqlem  26642  p1evtxdeq  26643  p1evtxdp1  26644  umgr2v2e  26655  vdiscusgrb  26660  vdegp1ai  26666  vdegp1bi  26667  ewlkle  26735  wksfval  26739  wksv  26749  wlk1ewlk  26770  uspgr2wlkeq  26776  wlkp1lem8  26811  upgr2pthnlp  26862  wlkiswwlks2  27008  wlksnwwlknvbij  27051  wlksnwwlknvbijOLD  27052  2pthdlem1  27076  wpthswwlks2on  27108  elwwlks2  27114  clwlkclwwlklem1  27148  clwwlknfi  27200  hashecclwwlkn1  27234  umgrhashecclwwlk  27235  clwwlkvbij  27288  clwwlkvbijOLDOLD  27289  clwwlkvbijOLD  27290  0wlkonlem1  27297  0wlkons1  27300  0pthon  27306  3wlkdlem4  27341  upgr3v3e3cycl  27359  trlsegvdeglem3  27401  trlsegvdeglem5  27403  eupth2lemb  27416  frgr3v  27456  frgr2wwlk1  27510  fusgreghash2wspv  27516  ex-lcm  27652  vsfval  27822  ipasslem7  28025  minvecolem2  28065  h2hcau  28170  h2hlm  28171  hlimadd  28384  hhsscms  28470  chocunii  28494  occllem  28496  eigposi  29029  leopnmid  29331  opsqrlem1  29333  hmopidmchi  29344  mdslj1i  29512  addltmulALT  29639  imadifxp  29745  xaddeq0  29851  fzodif2  29885  xrge0npcan  30025  gsumle  30110  xrge0tsmsd  30116  locfinreflem  30238  locfinref  30239  xpinpreima2  30284  cnre2csqlem  30287  tpr2rico  30289  ordtrestNEW  30298  ordtrest2NEW  30300  mndpluscn  30303  pnfneige0  30328  qqhghm  30363  qqhrhm  30364  qqhcn  30366  qqhucn  30367  rrhcn  30372  rrhre  30396  esumsplit  30446  esumpr  30459  esumfsup  30463  sigaclcu2  30514  pwsiga  30524  prsiga  30525  sigapildsys  30556  ldgenpisyslem1  30557  measvuni  30608  elmbfmvol2  30660  mbfmcnt  30661  sxbrsigalem1  30678  sxbrsiga  30683  omsfval  30687  carsgclctunlem2  30712  sibf0  30727  sitgclg  30735  sitmval  30742  eulerpartgbij  30765  eulerpartlemgh  30771  isrrvv  30836  rrvadd  30845  rrvmulc  30846  dstrvprob  30864  coinflipspace  30873  coinfliprv  30875  ballotlemfmpn  30887  ballotlem1ri  30927  sgnmulsgn  30942  plymul02  30954  signsplypnf  30958  signsply0  30959  signswrid  30966  prodfzo03  31012  itgexpif  31015  circlemethhgt  31052  hgt750lemb  31065  indispconn  31544  connpconn  31545  iccllysconn  31560  cvmopnlem  31588  cvmliftlem15  31608  cvmlift2lem3  31615  mrsubff  31737  mrsubccat  31743  circum  31895  noextend  32145  nosupbnd2lem1  32187  elhf2  32608  topdifinfindis  33512  icoreelrn  33527  finxpreclem2  33545  finixpnum  33709  matunitlindflem1  33720  matunitlindflem2  33721  poimirlem5  33729  poimirlem10  33734  poimirlem22  33746  poimirlem26  33750  poimirlem27  33751  poimirlem28  33752  poimirlem29  33753  poimirlem31  33755  poimirlem32  33756  mblfinlem3  33763  mblfinlem4  33764  ismblfin  33765  ovoliunnfl  33766  voliunnfl  33768  volsupnfl  33769  dvtan  33774  itg2addnclem  33775  ftc1anclem5  33803  dvasin  33810  dvreasin  33812  dvreacos  33813  areacirclem1  33814  areacirc  33819  bnd2lem  33903  prdsbnd  33905  cntotbnd  33908  cnpwstotbnd  33909  isdrngo2  34070  prter2  34662  eqlkr2  34882  tendoidcl  36551  cdlemk56  36753  dihpN  37118  mapdhval  37506  hlhillcs  37740  isnacs3  37776  diophrw  37825  lzenom  37836  diophin  37839  pellexlem5  37900  pw2f1ocnv  38106  dnnumch2  38117  kelac2lem  38136  kelac2  38137  dfac21  38138  pwfi2f1o  38168  frlmpwfi  38170  mpaaeu  38222  rngunsnply  38245  mendbas  38256  mendplusgfval  38257  mendmulrfval  38259  mendsca  38261  mendvscafval  38262  subrgacs  38272  sdrgacs  38273  cntzsdrg  38274  idomodle  38276  proot1ex  38281  deg1mhm  38287  itgpowd  38301  trclubgNEW  38426  dmtrcl  38435  rntrcl  38436  brfvidRP  38481  trclrelexplem  38504  relexp01min  38506  trclimalb2  38519  dssmapfvd  38812  ntrk0kbimka  38838  ntrrn  38921  dssmapntrcls  38927  amgm2d  39002  amgm3d  39003  amgm4d  39004  hashnzfzclim  39022  ofsubid  39024  ofdivrec  39026  dvconstbi  39034  fzisoeu  39996  iuneqfzuzlem  40031  sumnnodd  40343  liminfgf  40471  negcncfg  40575  cnfdmsn  40576  dvmptresicc  40615  itgcoscmulx  40665  stoweidlem13  40710  stoweidlem26  40723  stoweidlem34  40731  stoweidlem42  40739  stoweidlem44  40741  stoweidlem48  40745  stoweidlem62  40759  stoweid  40760  stirlinglem7  40777  stirlinglem11  40781  stirlinglem12  40782  dirkeritg  40799  dirkercncflem2  40801  dirkercncflem4  40803  fourierdlem16  40820  fourierdlem21  40825  fourierdlem22  40826  fourierdlem24  40828  fourierdlem48  40851  fourierdlem49  40852  fourierdlem62  40865  fourierdlem70  40873  fourierdlem80  40883  fourierdlem83  40886  fourierdlem85  40888  fourierdlem102  40905  fourierdlem104  40907  fourierdlem111  40914  fourierdlem112  40915  fourierdlem114  40917  etransclem18  40949  etransclem23  40954  etransclem24  40955  etransclem25  40956  etransclem35  40966  etransclem46  40977  ovolval5lem3  41351  setsidel  41922  iccpartipre  41933  iccpartiltu  41934  fmtnoprmfac2lem1  42054  mod42tp1mod8  42095  sfprmdvdsmersenne  42096  perfectALTVlem2  42207  stgoldbwt  42240  nnsum3primesgbe  42256  nnsum4primesodd  42260  nnsum4primesoddALTV  42261  nnsum4primeseven  42264  nnsum4primesevenALTV  42265  bgoldbtbndlem2  42270  upwlksfval  42285  sprval  42298  sprbisymrel  42318  uspgrbisymrelALT  42332  idmgmhm  42357  mgmplusgiopALT  42399  sgrp2sgrp  42433  isrnghm  42461  lidlmmgm  42494  zlidlring  42497  2zrngnmlid  42518  dfrngc2  42541  rnghmsscmap2  42542  rnghmsscmap  42543  rngchomfvalALTV  42553  rngcidALTV  42560  funcrngcsetcALT  42568  dfringc2  42587  rhmsscmap2  42588  rhmsscmap  42589  rhmsscrnghm  42595  rngcresringcat  42599  funcringcsetcALTV2lem8  42612  ringchomfvalALTV  42616  ringcidALTV  42623  funcringcsetclem8ALTV  42635  srhmsubc  42645  fldc  42652  rngcrescrhm  42654  rhmsubclem3  42657  srhmsubcALTV  42663  fldcALTV  42670  rngcrescrhmALTV  42672  altgsumbcALT  42700  zlmodzxzel  42702  zlmodzxzsubm  42706  zlmodzxzsub  42707  gsumpr  42708  scmsuppss  42722  ply1mulgsum  42747  dmatALTbas  42759  lcoop  42769  lincval0  42773  lco0  42785  linds0  42823  snlindsntorlem  42828  lmod1lem2  42846  lmod1lem3  42847  lmod1zr  42851  lmod1zrnlvec  42852  zlmodzxznm  42855  zlmodzxzldeplem4  42861  expnegico01  42877  pw2m1lepw2m1  42879  fldivexpfllog2  42928  blennnelnn  42939  blenpw2  42941  nnpw2pmod  42946  blennnt2  42952  nnolog2flm1  42953  digfval  42960  dignnld  42966  dig2nn0ld  42967  0dig2nn0e  42975  0dig2nn0o  42976  amgmwlem  43120  amgmlemALT  43121  amgmw2d  43122
  Copyright terms: Public domain W3C validator