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

Step	Hyp	Ref	Expression
1		mp1i.1	. . 3 ⊢ 𝜑
2		mp1i.2	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4	3	a1i 11	1 ⊢ (𝜒 → 𝜓)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  relsnopg  5461  poirr2  5762  fvrnressn  6679  isomin  6842  isoini  6843  mptmpt2opabbrd  7511  supp0  7564  suppval1  7565  suppssr  7591  dmtpos  7629  mpt2curryd  7660  oaabs2  7992  elqsecl  8066  mapsncnv  8171  boxcutc  8218  domunsncan  8329  unxpdom2  8437  sucxpdom  8438  findcard2d  8471  ac6sfi  8473  xpfi  8500  imafi  8528  snopfsupp  8567  fifo  8607  ordtypelem4  8695  oismo  8714  wofib  8719  brwdom2  8747  canthwdom  8753  cantnfval  8842  cantnflt  8846  cantnff  8848  cantnf0  8849  cantnfp1lem1  8852  cantnfp1lem3  8854  cantnflem1b  8860  cantnflem1  8863  cnfcom  8874  cnfcom2lem  8875  ranksnb  8967  updjudhcoinlf  9071  updjudhcoinrg  9072  updjud  9073  tskwe  9089  cardidm  9098  infxpenc  9154  fseqdom  9162  dfac8clem  9168  dfac12lem2  9281  infmap2  9355  isfin4-3  9452  fin23lem14  9470  fin23lem40  9488  isf34lem7  9516  isf34lem6  9517  fin1a2lem12  9548  hsmexlem4  9566  hsmexlem5  9567  ac5b  9615  alephexp1  9716  alephsuc3  9717  fpwwe2lem8  9774  fpwwe2lem13  9779  canthwe  9788  canthp1lem2  9790  gchcda1  9793  pwfseqlem5  9800  wunco  9870  prlem934  10170  supsrlem  10248  msqge0  10873  negfi  11301  ofnegsub  11348  ofsubge0  11349  xaddpnf1  12345  supxrmnf  12435  fz0sn0fz1  12751  injresinjlem  12883  fldiv4lem1div2  12933  uzindi  13076  seqfeq4  13144  seqof  13152  bcval5  13398  hashdomi  13459  hash1snb  13496  hashge2el2difr  13552  hashtpg  13556  fi1uzind  13568  ccatlen  13635  lswccatn0lsw  13651  ccatalpha  13653  eqs1  13672  s111  13675  swrd0  13723  swrdwrdsymb  13736  swrdspsleq  13739  wrdeqs1catOLD  13810  reps  13886  repsw0  13893  repswccat  13902  repswrevw  13903  lswcshw  13936  cshwsexa  13945  scshwfzeqfzo  13947  lsws2  14025  lsws3  14026  lsws4  14027  wrdlen2i  14063  relexpsucnnr  14142  relexpaddg  14170  shftfib  14189  limsupcl  14581  limsupgf  14583  limsupval2  14588  isercolllem3  14774  modfsummods  14899  ackbijnn  14934  supcvg  14962  fprodfac  15076  fprodmodd  15100  fallfac0  15131  bpoly4  15162  ege2le3  15192  rpnnen2lem5  15321  ruclem11  15343  fsumdvds  15407  fproddvdsd  15433  mod2eq1n2dvds  15445  oddnn02np1  15446  oddge22np1  15447  evennn02n  15448  evennn2n  15449  bitsinv2  15538  sadaddlem  15561  smupf  15573  smup0  15574  smu01lem  15580  3lcm2e6woprm  15701  6lcm4e12  15702  lcmfunsnlem1  15723  lcmfunsnlem2lem1  15724  lcmfunsnlem2  15726  coprmprod  15747  isprm6  15797  hashdvds  15851  phisum  15866  reumodprminv  15880  prmreclem6  15996  vdwlem13  16068  ramtlecl  16075  0ram  16095  prmdvdsprmo  16117  fvprmselgcd1  16120  prmgaplcmlem1  16126  prmgaplem7  16132  prmgaplcm  16135  cshwshashnsame  16176  prmlem0  16178  wunndx  16243  prdsval  16468  xpsbas  16587  xpsadd  16589  xpsmul  16590  xpssca  16591  xpsvsca  16592  xpsless  16593  xpsle  16594  mreexexlem2d  16658  mreacs  16671  acsfn  16672  isofn  16787  ciclcl  16814  cicrcl  16815  cicsym  16816  cicer  16818  idfu2nd  16889  idfucl  16893  fucsect  16984  initoeu2lem1  17016  initoeu2lem2  17017  setccatid  17086  setcepi  17090  catchomfval  17100  estrccatid  17124  estrreslem1  17129  estrreslem2  17130  estrresOLD  17131  estrres  17132  funcestrcsetclem8  17140  fullestrcsetc  17144  embedsetcestrclem  17150  funcsetcestrclem8  17155  uncfval  17227  oduglb  17492  odumeet  17493  odulub  17494  odujoin  17495  isipodrs  17514  fpwipodrs  17517  isacs5lem  17522  idmhm  17697  submacs  17718  frmdup1  17755  mgmnsgrpex  17772  mulgneg2  17927  subgacs  17980  nsgacs  17981  idrespermg  18181  psgnunilem5  18264  psgnunilem5OLD  18265  psgnsn  18291  odf1o2  18339  frgpuplem  18538  cygctb  18646  gsumzunsnd  18708  gsum2dlem2  18723  gsummptnn0fz  18735  gsummptnn0fzOLD  18736  dprdsubg  18777  dmdprdsplit2lem  18798  dmdprdpr  18802  dprdpr  18803  dpjeq  18812  ablfac1eulem  18825  pgpfac1lem2  18828  pgpfaclem1  18834  srgbinomlem4  18897  unitgrp  19021  isirred  19053  brric  19100  mptscmfsupp0  19284  lssacs  19326  pwssplit1  19418  lbsextlem2  19520  lbsextlem3  19521  isnzr2hash  19625  0ring01eqbi  19634  rng1nnzr  19635  psrass1lem  19738  psrlidm  19764  resspsradd  19777  resspsrmul  19778  resspsrvsca  19779  mplcoe5lem  19828  ltbwe  19833  coe1fsupp  19944  psropprmul  19968  coe1add  19994  coe1mul2lem1  19997  coe1tm  20003  cply1coe0bi  20030  evls1rhmlem  20046  evl1sca  20058  evl1var  20060  pf1mpf  20076  pf1ind  20079  xrsmcmn  20129  xrs1mnd  20144  xrs10  20145  gsumfsum  20173  zringlpir  20197  zringcyg  20199  zndvds  20257  regsumsupp  20329  uvcvv1  20495  lsslinds  20537  matmulr  20611  ofco2  20625  mat0dimbas0  20640  mat1dimelbas  20645  mat1f1o  20652  dmatval  20666  scmatghm  20707  mavmul0  20726  mavmul0g  20727  m1detdiag  20771  mdetunilem9  20794  maducoeval2  20814  madugsum  20817  smadiadetlem0  20836  smadiadetlem1a  20838  smadiadetlem4  20844  smadiadetglem1  20846  smadiadetglem2  20847  smadiadetg  20848  cramer0  20866  cpmat  20884  mat2pmatfval  20898  cpm2mfval  20924  m2cpminvid2lem  20929  pmatcollpw3fi1lem2  20962  pmatcollpw3fi1  20963  idpm2idmp  20976  pm2mpmhmlem2  20994  chpmatfval  21005  chfacfscmulfsupp  21034  chfacfpmmulfsupp  21038  cpmidpmatlem2  21046  cpmadugsumlemF  21051  cpmidgsum2  21054  cpmadumatpolylem1  21056  cayhamlem3  21062  cayhamlem4  21063  indistopon  21176  mreclatdemoBAD  21271  mnfnei  21396  resthauslem  21538  sshauslem  21547  discmp  21572  connima  21599  1stcfb  21619  ptbasfi  21755  hauseqlcld  21820  xkoptsub  21828  xkofvcn  21858  idqtop  21880  tgqtop  21886  kqdisj  21906  xpstopnlem1  21983  xpstopnlem2  21985  ufildom1  22100  alexsubb  22220  alexsubALTlem3  22223  ptcmplem2  22227  ptcmplem3  22228  tmdgsum  22269  ustneism  22397  ustuqtop1  22415  iducn  22457  prdsmet  22545  imasdsf1olem  22548  xpsxmet  22555  xpsdsval  22556  xpsmet  22557  prdsbl  22666  met1stc  22696  prdsxmslem2  22704  xpsxms  22709  xpsms  22710  psmetutop  22742  dscmet  22747  nmoffn  22885  nmofval  22888  nmolb  22891  nmof  22893  cnbl0  22947  xrsmopn  22985  xrge0gsumle  23006  xrge0tsms  23007  negfcncf  23092  cnrehmeo  23122  lebnum  23133  xlebnum  23134  reparphti  23166  pcopt  23191  pcopt2  23192  pcorevcl  23194  pcorevlem  23195  pi1xfrval  23223  pi1xfrcnvlem  23225  pi1xfrcnv  23226  pi1cof  23228  pi1coval  23229  nmhmcn  23289  cphsubrglem  23346  csscld  23417  cmetcaulem  23456  cmpcmet  23487  csschl  23544  rrxplusgvscavalb  23563  rrxsca  23564  ehleudis  23586  divcncf  23613  ovolunlem1  23663  ovolicc2lem4  23686  ioovolcl  23736  ioorcl2  23738  uniioovol  23745  uniioombllem4  23752  uniioombllem5  23753  uniioombllem6  23754  dyadmbllem  23765  mbfsub  23828  itg1climres  23880  xrge0f  23897  itg2ge0  23901  itg2i1fseq2  23922  ibl0  23952  ellimc2  24040  limcflf  24044  dvreslem  24072  dvidlem  24078  dvid  24080  cpnres  24099  dvaddbr  24100  dvmulbr  24101  dvfre  24113  dvexp  24115  dvrec  24117  dvmptid  24119  dvmptc  24120  dvmptntr  24133  dvexp3  24140  dvlipcn  24156  dveq0  24162  dv11cn  24163  lhop2  24177  ftc1a  24199  tdeglem1  24217  tdeglem3  24218  tdeglem4  24219  tdeglem2  24220  mdeg0  24229  mdegle0  24236  ply1remlem  24321  plypf1  24367  coe0  24411  dvply1  24438  elqaalem3  24475  aaliou2b  24495  aaliou3lem8  24499  aaliou3lem7  24503  taylfvallem  24511  taylf  24514  tayl0  24515  taylpfval  24518  taylply  24522  dvtaylp  24523  taylthlem1  24526  taylthlem2  24527  ulmdvlem1  24553  ulmdvlem2  24554  ulmdvlem3  24555  radcnvcl  24570  psercnlem2  24577  psercn  24579  pserdv  24582  abelthlem3  24586  abelth  24594  sincn  24597  coscn  24598  reefgim  24603  tangtx  24657  pige3  24669  cosordlem  24677  logcn  24792  dvlog  24796  advlog  24799  advlogexp  24800  logtayl  24805  logccv  24808  dvcxp1  24883  dvcncxp1  24886  cxpcn3lem  24890  cxpcn3  24891  resqrtcn  24892  sqrtcn  24893  loglesqrt  24901  logbfval  24930  logblog  24932  isosctrlem2  24959  dquartlem1  24991  quart  25001  atancj  25050  efiatan  25052  atantan  25063  atanbndlem  25065  atansopn  25072  dvatan  25075  atantayl  25077  leibpilem2  25081  leibpi  25082  log2tlbnd  25085  rlimcnp2  25106  efrlim  25109  divsqrtsumlem  25119  jensenlem1  25126  jensenlem2  25127  jensen  25128  amgmlem  25129  amgm  25130  emcllem4  25138  emcllem7  25141  lgamcvg2  25194  gamcvg2lem  25198  wilthlem2  25208  wilthlem3  25209  basellem6  25225  chtrpcl  25314  ppiltx  25316  1sgm2ppw  25338  chtlepsi  25344  chpub  25358  logfacbnd3  25361  logfacrlim  25362  perfectlem2  25368  dchrelbas2  25375  dchrabs  25398  dchrhash  25409  bposlem7  25428  lgsdir2lem5  25467  lgsqrlem1  25484  gausslemma2dlem5  25509  gausslemma2dlem6  25510  lgseisenlem4  25516  lgsquad2lem1  25522  lgsquad3  25525  chpo1ub  25582  vmadivsumb  25585  rpvmasumlem  25589  dchrisumlem2  25592  dchrmusumlema  25595  dchrvmasumlem2  25600  dchrvmasumlema  25602  dchrvmasumiflem1  25603  dchrisum0flblem1  25610  dchrisum0lem1  25618  rplogsum  25629  mudivsum  25632  logdivsum  25635  mulog2sumlem2  25637  vmalogdivsum2  25640  2vmadivsumlem  25642  log2sumbnd  25646  selberglem2  25648  selbergb  25651  selberg2lem  25652  selberg2b  25654  selberg3lem1  25659  selberg4lem1  25662  selberg4  25663  pntrsumo1  25667  pntrlog2bndlem2  25680  pntrlog2bndlem3  25681  pntrlog2bndlem4  25682  pntrlog2bndlem5  25683  pntibndlem1  25691  pntibndlem2  25693  pntibndlem3  25694  pntlemb  25699  pntlemr  25704  pntlemf  25707  pntlem3  25711  pnt  25716  qabvle  25727  padicabv  25732  ostth1  25735  istrkg2ld  25772  tgldimor  25814  tgcgr4  25843  motgrp  25855  perpln1  26022  perpln2  26023  isperp  26024  snstrvtxval  26335  snstriedgval  26336  isuhgrop  26368  uhgrunop  26373  uhgrstrrepe  26376  upgrop  26392  upgrunop  26417  umgrunop  26419  isusgrs  26455  isuspgrop  26460  isusgrop  26461  usgrop  26462  usgrstrrepe  26532  uspgr1ewop  26545  usgr2v1e2w  26549  uhgrspan1  26600  upgrres  26603  umgrres  26604  usgrres  26605  upgrres1  26610  umgrres1  26611  usgrres1  26612  isfusgrcl  26618  fusgredgfi  26622  usgr1v0e  26623  nbgrval  26633  nbusgrf1o1  26668  nbfusgrlevtxm2  26676  uvtx01vtx  26695  usgrexilem  26738  usgrexi  26739  cusgrexi  26741  structtousgr  26743  structtocusgr  26744  cusgrres  26746  cusgrfilem3  26755  sizusglecusg  26761  vtxdgfval  26765  vtxdgop  26768  vtxdgf  26769  vtxdlfgrval  26783  vtxd0nedgb  26786  vtxdusgr0edgnelALT  26794  1loopgrvd0  26802  1egrvtxdg1  26807  1egrvtxdg0  26809  p1evtxdeqlem  26810  p1evtxdeq  26811  p1evtxdp1  26812  umgr2v2e  26823  vdiscusgrb  26828  vdegp1ai  26834  vdegp1bi  26835  ewlkle  26903  wksfval  26907  wksv  26917  wlk1ewlk  26937  uspgr2wlkeq  26943  wlkp1lem8  26981  upgr2pthnlp  27034  wlkiswwlks2  27174  wlksnwwlknvbij  27230  wlksnwwlknvbijOLD  27231  2pthdlem1  27259  wpthswwlks2on  27290  elwwlks2  27295  clwlkclwwlklem1  27328  clwwlknfi  27390  hashecclwwlkn1  27430  umgrhashecclwwlk  27431  clwwlkvbij  27488  clwwlkvbijOLD  27489  0wlkonlem1  27494  0wlkons1  27497  0pthon  27503  3wlkdlem4  27538  upgr3v3e3cycl  27556  trlsegvdeglem3  27599  trlsegvdeglem5  27601  eupth2lemb  27614  frgr3v  27656  frgr2wwlk1  27710  fusgreghash2wspv  27716  ex-lcm  27873  vsfval  28043  ipasslem7  28246  minvecolem2  28286  h2hcau  28391  h2hlm  28392  hlimadd  28605  hhsscms  28691  chocunii  28715  occllem  28717  eigposi  29250  leopnmid  29552  opsqrlem1  29554  hmopidmchi  29565  mdslj1i  29733  addltmulALT  29860  imadifxp  29961  xaddeq0  30065  fzodif2  30099  xrge0npcan  30239  gsumle  30324  xrge0tsmsd  30330  locfinreflem  30452  locfinref  30453  xpinpreima2  30498  cnre2csqlem  30501  tpr2rico  30503  ordtrestNEW  30512  ordtrest2NEW  30514  mndpluscn  30517  pnfneige0  30542  qqhghm  30577  qqhrhm  30578  qqhcn  30580  qqhucn  30581  rrhcn  30586  rrhre  30610  esumsplit  30660  esumpr  30673  esumfsup  30677  sigaclcu2  30728  pwsiga  30738  prsiga  30739  sigapildsys  30770  ldgenpisyslem1  30771  measvuni  30822  elmbfmvol2  30874  mbfmcnt  30875  sxbrsigalem1  30892  sxbrsiga  30897  omsfval  30901  carsgclctunlem2  30926  sibf0  30941  sitgclg  30949  sitmval  30956  eulerpartgbij  30979  eulerpartlemgh  30985  isrrvv  31051  rrvadd  31060  rrvmulc  31061  dstrvprob  31079  coinflipspace  31088  coinfliprv  31090  ballotlemfmpn  31102  ballotlem1ri  31142  sgnmulsgn  31157  plymul02  31170  signsplypnf  31174  signsply0  31175  signswrid  31182  prodfzo03  31230  itgexpif  31233  circlemethhgt  31270  hgt750lemb  31283  indispconn  31762  connpconn  31763  iccllysconn  31778  cvmopnlem  31806  cvmliftlem15  31826  cvmlift2lem3  31833  mrsubff  31955  mrsubccat  31961  circum  32112  noextend  32358  nosupbnd2lem1  32400  elhf2  32821  topdifinfindis  33739  icoreelrn  33754  finxpreclem2  33772  finixpnum  33937  matunitlindflem1  33949  matunitlindflem2  33950  poimirlem5  33958  poimirlem10  33963  poimirlem22  33975  poimirlem26  33979  poimirlem27  33980  poimirlem28  33981  poimirlem29  33982  poimirlem31  33984  poimirlem32  33985  mblfinlem3  33992  mblfinlem4  33993  ismblfin  33994  ovoliunnfl  33995  voliunnfl  33997  volsupnfl  33998  dvtan  34003  itg2addnclem  34004  ftc1anclem5  34032  dvasin  34039  dvreasin  34041  dvreacos  34042  areacirclem1  34043  areacirc  34048  bnd2lem  34132  prdsbnd  34134  cntotbnd  34137  cnpwstotbnd  34138  isdrngo2  34299  prter2  34956  eqlkr2  35175  tendoidcl  36844  cdlemk56  37046  dihpN  37411  mapdhval  37799  hlhillcs  38033  isnacs3  38117  diophrw  38166  lzenom  38177  diophin  38180  pellexlem5  38241  pw2f1ocnv  38447  dnnumch2  38458  kelac2lem  38477  kelac2  38478  dfac21  38479  pwfi2f1o  38509  frlmpwfi  38511  mpaaeu  38563  rngunsnply  38586  mendbas  38597  mendplusgfval  38598  mendmulrfval  38600  mendsca  38602  mendvscafval  38603  subrgacs  38613  sdrgacs  38614  cntzsdrg  38615  idomodle  38617  proot1ex  38622  deg1mhm  38628  itgpowd  38642  trclubgNEW  38766  dmtrcl  38775  rntrcl  38776  brfvidRP  38821  trclrelexplem  38844  relexp01min  38846  trclimalb2  38859  dssmapfvd  39151  ntrk0kbimka  39177  ntrrn  39260  dssmapntrcls  39266  amgm2d  39341  amgm3d  39342  amgm4d  39343  hashnzfzclim  39361  ofsubid  39363  ofdivrec  39365  dvconstbi  39373  fzisoeu  40312  iuneqfzuzlem  40347  sumnnodd  40657  liminfgf  40785  negcncfg  40889  cnfdmsn  40890  dvmptresicc  40929  itgcoscmulx  40979  stoweidlem13  41024  stoweidlem26  41037  stoweidlem34  41045  stoweidlem42  41053  stoweidlem44  41055  stoweidlem48  41059  stoweidlem62  41073  stoweid  41074  stirlinglem7  41091  stirlinglem11  41095  stirlinglem12  41096  dirkeritg  41113  dirkercncflem2  41115  dirkercncflem4  41117  fourierdlem16  41134  fourierdlem21  41139  fourierdlem22  41140  fourierdlem24  41142  fourierdlem48  41165  fourierdlem49  41166  fourierdlem62  41179  fourierdlem70  41187  fourierdlem80  41197  fourierdlem83  41200  fourierdlem85  41202  fourierdlem102  41219  fourierdlem104  41221  fourierdlem111  41228  fourierdlem112  41229  fourierdlem114  41231  etransclem18  41263  etransclem23  41268  etransclem24  41269  etransclem25  41270  etransclem35  41280  etransclem46  41291  ovolval5lem3  41662  setsidel  42234  iccpartipre  42245  iccpartiltu  42246  fmtnoprmfac2lem1  42308  mod42tp1mod8  42349  sfprmdvdsmersenne  42350  perfectALTVlem2  42461  stgoldbwt  42494  nnsum3primesgbe  42510  nnsum4primesodd  42514  nnsum4primesoddALTV  42515  nnsum4primeseven  42518  nnsum4primesevenALTV  42519  bgoldbtbndlem2  42524  isomuspgrlem2  42551  ushrisomgr  42559  upwlksfval  42563  sprval  42576  sprbisymrel  42596  uspgrbisymrelALT  42610  idmgmhm  42635  mgmplusgiopALT  42677  sgrp2sgrp  42711  isrnghm  42739  lidlmmgm  42772  zlidlring  42775  2zrngnmlid  42796  dfrngc2  42819  rnghmsscmap2  42820  rnghmsscmap  42821  rngchomfvalALTV  42831  rngcidALTV  42838  funcrngcsetcALT  42846  dfringc2  42865  rhmsscmap2  42866  rhmsscmap  42867  rhmsscrnghm  42873  rngcresringcat  42877  funcringcsetcALTV2lem8  42890  ringchomfvalALTV  42894  ringcidALTV  42901  funcringcsetclem8ALTV  42913  srhmsubc  42923  fldc  42930  rngcrescrhm  42932  rhmsubclem3  42935  srhmsubcALTV  42941  fldcALTV  42948  rngcrescrhmALTV  42950  altgsumbcALT  42978  zlmodzxzel  42980  zlmodzxzsubm  42984  zlmodzxzsub  42985  gsumpr  42986  scmsuppss  43000  ply1mulgsum  43025  dmatALTbas  43037  lcoop  43047  lincval0  43051  lco0  43063  linds0  43101  snlindsntorlem  43106  lmod1lem2  43124  lmod1lem3  43125  lmod1zr  43129  lmod1zrnlvec  43130  zlmodzxznm  43133  zlmodzxzldeplem4  43139  expnegico01  43155  pw2m1lepw2m1  43157  fldivexpfllog2  43206  blennnelnn  43217  blenpw2  43219  nnpw2pmod  43224  blennnt2  43230  nnolog2flm1  43231  digfval  43238  dignnld  43244  dig2nn0ld  43245  0dig2nn0e  43253  0dig2nn0o  43254  rrxlines  43284  eenglngeehlnmlem1  43288  eenglngeehlnmlem2  43289  rrxsphere  43300  line2  43304  line2x  43306  line2y  43307  amgmwlem  43444  amgmlemALT  43445  amgmw2d  43446