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:  poirr2  5439  fvrnressn  6333  isomin  6487  isoini  6488  supp0  7187  suppval1  7188  suppssr  7213  dmtpos  7251  mpt2curryd  7282  oaabs2  7612  elqsecl  7688  mapsncnv  7790  boxcutc  7837  domunsncan  7945  unxpdom2  8053  sucxpdom  8054  findcard2d  8087  ac6sfi  8089  xpfi  8116  imafi  8142  snopfsupp  8181  fifo  8221  ordtypelem4  8309  oismo  8328  wofib  8333  brwdom2  8361  canthwdom  8367  cantnfval  8448  cantnflt  8452  cantnff  8454  cantnf0  8455  cantnfp1lem1  8458  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1  8469  cnfcom  8480  cnfcom2lem  8481  ranksnb  8573  tskwe  8659  cardidm  8668  infxpenc  8724  fseqdom  8732  dfac8clem  8738  dfac12lem2  8849  infmap2  8923  isfin4-3  9020  fin23lem14  9038  fin23lem40  9056  isf34lem7  9084  isf34lem6  9085  fin1a2lem12  9116  hsmexlem4  9134  hsmexlem5  9135  ac5b  9183  alephexp1  9280  alephsuc3  9281  fpwwe2lem8  9338  fpwwe2lem13  9343  canthwe  9352  canthp1lem2  9354  gchcda1  9357  pwfseqlem5  9364  wunco  9434  prlem934  9734  supsrlem  9811  msqge0  10428  negfi  10850  ofnegsub  10895  ofsubge0  10896  xaddpnf1  11931  supxrmnf  12019  fz0sn0fz1  12325  injresinjlem  12450  fldiv4lem1div2  12500  uzindi  12643  seqfeq4  12712  seqof  12720  bcval5  12967  hashdomi  13030  hash1snb  13068  hashge2el2difr  13118  hashtpg  13121  fi1uzind  13134  fi1uzindOLD  13140  ccatlen  13213  lswccatn0lsw  13226  ccatalpha  13228  eqs1  13245  s111  13248  swrd0  13286  swrdspsleq  13301  wrdeqs1cat  13326  reps  13368  repsw0  13375  repswccat  13383  repswrevw  13384  lswcshw  13412  cshwsexa  13421  scshwfzeqfzo  13423  lsws2  13499  lsws3  13500  lsws4  13501  wrdlen2i  13534  relexpsucnnr  13613  relexpaddg  13641  shftfib  13660  limsupcl  14052  limsupgf  14054  limsupval2  14059  isercolllem3  14245  modfsummods  14366  ackbijnn  14399  supcvg  14427  fprodfac  14542  fprodmodd  14567  fallfac0  14598  bpoly4  14629  ege2le3  14659  rpnnen2lem5  14786  ruclem11  14808  fsumdvds  14868  fproddvdsd  14897  mod2eq1n2dvds  14909  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  bitsinv2  15003  sadaddlem  15026  smupf  15038  smup0  15039  smu01lem  15045  3lcm2e6woprm  15166  6lcm4e12  15167  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  coprmprod  15213  isprm6  15264  hashdvds  15318  phisum  15333  reumodprminv  15347  prmreclem6  15463  vdwlem13  15535  ramtlecl  15542  0ram  15562  prmdvdsprmo  15584  fvprmselgcd1  15587  prmgaplcmlem1  15593  prmgaplem7  15599  prmgaplcm  15602  cshwshashnsame  15648  prmlem0  15650  wunndx  15711  prdsval  15938  xpsbas  16057  xpsadd  16059  xpsmul  16060  xpssca  16061  xpsvsca  16062  xpsless  16063  xpsle  16064  mreexexlem2d  16128  mreacs  16142  acsfn  16143  isofn  16258  ciclcl  16285  cicrcl  16286  cicsym  16287  cicer  16289  idfu2nd  16360  idfucl  16364  fucsect  16455  initoeu2lem1  16487  initoeu2lem2  16488  setccatid  16557  setcepi  16561  catchomfval  16571  estrccatid  16595  estrreslem1  16600  estrreslem2  16601  estrres  16602  funcestrcsetclem8  16610  fullestrcsetc  16614  embedsetcestrclem  16620  funcsetcestrclem8  16625  uncfval  16697  oduglb  16962  odumeet  16963  odulub  16964  odujoin  16965  isipodrs  16984  fpwipodrs  16987  isacs5lem  16992  idmhm  17167  submacs  17188  frmdup1  17224  mgmnsgrpex  17241  mulgneg2  17398  subgacs  17452  nsgacs  17453  idrespermg  17654  psgnunilem5  17737  psgnsn  17763  odf1o2  17811  frgpuplem  18008  cygctb  18116  gsumzunsnd  18178  gsum2dlem2  18193  gsummptnn0fz  18205  dprdsubg  18246  dmdprdsplit2lem  18267  dmdprdpr  18271  dprdpr  18272  dpjeq  18281  ablfac1eulem  18294  pgpfac1lem2  18297  pgpfaclem1  18303  srgbinomlem4  18366  unitgrp  18490  isirred  18522  brric  18567  mptscmfsupp0  18751  lssacs  18788  pwssplit1  18880  lbsextlem2  18980  lbsextlem3  18981  isnzr2hash  19085  0ring01eqbi  19094  rng1nnzr  19095  psrass1lem  19198  psrlidm  19224  resspsradd  19237  resspsrmul  19238  resspsrvsca  19239  mplcoe5lem  19288  ltbwe  19293  coe1fsupp  19405  psropprmul  19429  coe1add  19455  coe1mul2lem1  19458  coe1tm  19464  cply1coe0bi  19491  evls1rhmlem  19507  evl1sca  19519  evl1var  19521  pf1mpf  19537  pf1ind  19540  xrsmcmn  19588  xrs1mnd  19603  xrs10  19604  gsumfsum  19632  zringlpir  19656  zringcyg  19658  zndvds  19717  regsumsupp  19787  uvcvv1  19947  lsslinds  19989  matmulr  20063  ofco2  20076  mat0dimbas0  20091  mat1dimelbas  20096  mat1f1o  20103  dmatval  20117  scmatghm  20158  mavmul0  20177  mavmul0g  20178  m1detdiag  20222  mdetunilem9  20245  maducoeval2  20265  madugsum  20268  smadiadetlem0  20286  smadiadetlem1a  20288  smadiadetlem4  20294  smadiadetglem1  20296  smadiadetglem2  20297  smadiadetg  20298  cramer0  20315  cpmat  20333  mat2pmatfval  20347  cpm2mfval  20373  m2cpminvid2lem  20378  pmatcollpw3fi1lem2  20411  pmatcollpw3fi1  20412  idpm2idmp  20425  pm2mpmhmlem2  20443  chpmatfval  20454  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  cpmidpmatlem2  20495  cpmadugsumlemF  20500  cpmidgsum2  20503  cpmadumatpolylem1  20505  cayhamlem3  20511  cayhamlem4  20512  indistopon  20615  mreclatdemoBAD  20710  mnfnei  20835  resthauslem  20977  sshauslem  20986  discmp  21011  conima  21038  1stcfb  21058  ptbasfi  21194  hauseqlcld  21259  xkoptsub  21267  xkofvcn  21297  idqtop  21319  tgqtop  21325  kqdisj  21345  xpstopnlem1  21422  xpstopnlem2  21424  ufildom1  21540  alexsubb  21660  alexsubALTlem3  21663  ptcmplem2  21667  ptcmplem3  21668  tmdgsum  21709  ustneism  21837  ustuqtop1  21855  iducn  21897  prdsmet  21985  imasdsf1olem  21988  xpsxmet  21995  xpsdsval  21996  xpsmet  21997  prdsbl  22106  met1stc  22136  prdsxmslem2  22144  xpsxms  22149  xpsms  22150  psmetutop  22182  dscmet  22187  nmoffn  22325  nmofval  22328  nmolb  22331  nmof  22333  cnbl0  22387  xrsmopn  22423  xrge0gsumle  22444  xrge0tsms  22445  negfcncf  22530  cnrehmeo  22560  lebnum  22571  xlebnum  22572  reparphti  22605  pcopt  22630  pcopt2  22631  pcorevcl  22633  pcorevlem  22634  pi1xfrval  22662  pi1xfrcnvlem  22664  pi1xfrcnv  22665  pi1cof  22667  pi1coval  22668  nmhmcn  22728  cphsubrglem  22785  csscld  22856  cmetcaulem  22894  cmpcmet  22924  ovolunlem1  23072  ovolicc2lem4  23095  ioovolcl  23144  ioorcl2  23146  uniioovol  23153  uniioombllem4  23160  uniioombllem5  23161  uniioombllem6  23162  dyadmbllem  23173  mbfsub  23235  itg1climres  23287  xrge0f  23304  itg2ge0  23308  itg2i1fseq2  23329  ibl0  23359  ellimc2  23447  limcflf  23451  dvreslem  23479  dvidlem  23485  dvid  23487  cpnres  23506  dvaddbr  23507  dvmulbr  23508  dvfre  23520  dvexp  23522  dvrec  23524  dvmptid  23526  dvmptc  23527  dvmptntr  23540  dvexp3  23545  dvlipcn  23561  dveq0  23567  dv11cn  23568  lhop2  23582  ftc1a  23604  tdeglem1  23622  tdeglem3  23623  tdeglem4  23624  tdeglem2  23625  mdeg0  23634  mdegle0  23641  ply1remlem  23726  plypf1  23772  coe0  23816  dvply1  23843  elqaalem3  23880  aaliou2b  23900  aaliou3lem8  23904  aaliou3lem7  23908  taylfvallem  23916  taylf  23919  tayl0  23920  taylpfval  23923  taylply  23927  dvtaylp  23928  taylthlem1  23931  taylthlem2  23932  ulmdvlem1  23958  ulmdvlem2  23959  ulmdvlem3  23960  radcnvcl  23975  psercnlem2  23982  psercn  23984  pserdv  23987  abelthlem3  23991  abelth  23999  sincn  24002  coscn  24003  reefgim  24008  tangtx  24061  pige3  24073  cosordlem  24081  logcn  24193  dvlog  24197  advlog  24200  advlogexp  24201  logtayl  24206  logccv  24209  dvcxp1  24281  dvcncxp1  24284  cxpcn3lem  24288  cxpcn3  24289  resqrtcn  24290  sqrtcn  24291  loglesqrt  24299  logbfval  24328  logblog  24330  isosctrlem2  24349  dquartlem1  24378  quart  24388  atancj  24437  efiatan  24439  atantan  24450  atanbndlem  24452  atansopn  24459  dvatan  24462  atantayl  24464  leibpilem2  24468  leibpi  24469  log2tlbnd  24472  rlimcnp2  24493  efrlim  24496  divsqrtsumlem  24506  jensenlem1  24513  jensenlem2  24514  jensen  24515  amgmlem  24516  amgm  24517  emcllem4  24525  emcllem7  24528  lgamcvg2  24581  gamcvg2lem  24585  wilthlem2  24595  wilthlem3  24596  basellem6  24612  chtrpcl  24701  ppiltx  24703  1sgm2ppw  24725  chtlepsi  24731  chpub  24745  logfacbnd3  24748  logfacrlim  24749  perfectlem2  24755  dchrelbas2  24762  dchrabs  24785  dchrhash  24796  bposlem7  24815  lgsdir2lem5  24854  lgsqrlem1  24871  gausslemma2dlem5  24896  gausslemma2dlem6  24897  lgseisenlem4  24903  lgsquad2lem1  24909  lgsquad3  24912  chpo1ub  24969  vmadivsumb  24972  rpvmasumlem  24976  dchrisumlem2  24979  dchrmusumlema  24982  dchrvmasumlem2  24987  dchrvmasumlema  24989  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0lem1  25005  rplogsum  25016  mudivsum  25019  logdivsum  25022  mulog2sumlem2  25024  vmalogdivsum2  25027  2vmadivsumlem  25029  log2sumbnd  25033  selberglem2  25035  selbergb  25038  selberg2lem  25039  selberg2b  25041  selberg3lem1  25046  selberg4lem1  25049  selberg4  25050  pntrsumo1  25054  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntibndlem1  25078  pntibndlem2  25080  pntibndlem3  25081  pntlemb  25086  pntlemr  25091  pntlemf  25094  pntlem3  25098  pnt  25103  qabvle  25114  padicabv  25119  ostth1  25122  istrkg2ld  25159  tgldimor  25197  tgcgr4  25226  motgrp  25238  perpln1  25405  perpln2  25406  isperp  25407  snstrvtxval  25712  snstriedgval  25713  isuhgrop  25736  uhgrunop  25741  uhgrstrrepe  25745  upgrunop  25785  umgrunop  25787  edgastruct  25797  uhgrares  25837  umgrares  25853  edgopval  25869  usgrares  25898  nbgraop  25952  nbgraopALT  25953  nbgraf1o0  25975  cusgra0v  25989  cusgra1v  25990  cusgraexilem2  25996  sizeusglecusg  26014  isuvtx  26016  2trllemH  26082  wlkntrllem3  26091  2wlklem1  26127  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  constr3trllem3  26180  constr3pthlem3  26185  wwlkn  26210  wlkiswwlk2  26225  wwlkn0s  26233  usg2wlkeq  26236  wlknwwlknvbij  26268  clwwlkn  26295  clwwlkn2  26303  clwlkisclwwlklem2  26314  clwwlkvbij  26329  hashecclwwlkn1  26361  usghashecclwwlk  26362  vdgr0  26427  rusgrasn  26472  eupatrl  26495  eupares  26502  vdegp1ai  26511  vdegp1bi  26512  frgra3v  26529  frgrancvvdeqlem9  26568  frgrancvvdgeq  26570  frg2wot1  26584  usgreghash2spotv  26593  extwwlkfablem2  26605  numclwwlkovf2  26611  ex-lcm  26707  vsfval  26872  ipasslem7  27075  minvecolem2  27115  h2hcau  27220  h2hlm  27221  hlimadd  27434  hhsscms  27520  chocunii  27544  occllem  27546  leopnmid  28381  opsqrlem1  28383  hmopidmchi  28394  mdslj1i  28562  addltmulALT  28689  imadifxp  28796  xaddeq0  28907  xrge0npcan  29025  gsumle  29110  xrge0tsmsd  29116  locfinreflem  29235  locfinref  29236  xpinpreima2  29281  cnre2csqlem  29284  tpr2rico  29286  ordtrestNEW  29295  ordtrest2NEW  29297  mndpluscn  29300  pnfneige0  29325  qqhghm  29360  qqhrhm  29361  qqhcn  29363  qqhucn  29364  rrhcn  29369  rrhre  29393  esumsplit  29442  esumpr  29455  esumfsup  29459  sigaclcu2  29510  pwsiga  29520  prsiga  29521  sigapildsys  29552  ldgenpisyslem1  29553  measvuni  29604  elmbfmvol2  29656  mbfmcnt  29657  sxbrsigalem1  29674  sxbrsiga  29679  omsfval  29683  carsgclctunlem2  29708  sibf0  29723  sitgclg  29731  sitmval  29738  eulerpartgbij  29761  eulerpartlemgh  29767  isrrvv  29832  rrvadd  29841  rrvmulc  29842  dstrvprob  29860  coinflipspace  29869  coinfliprv  29871  ballotlemfmpn  29883  ballotlem1ri  29923  sgnmulsgn  29938  plymul02  29949  signsplypnf  29953  signsply0  29954  signswrid  29961  indispcon  30470  conpcon  30471  iccllyscon  30486  cvmopnlem  30514  cvmliftlem15  30534  cvmlift2lem3  30541  mrsubff  30663  mrsubccat  30669  circum  30822  elhf2  31452  topdifinfindis  32370  icoreelrn  32385  finxpreclem2  32403  finixpnum  32564  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem5  32584  poimirlem10  32589  poimirlem22  32601  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  dvtan  32630  itg2addnclem  32631  ftc1anclem5  32659  dvasin  32666  dvreasin  32668  dvreacos  32669  areacirclem1  32670  areacirc  32675  bnd2lem  32760  prdsbnd  32762  cntotbnd  32765  cnpwstotbnd  32766  isdrngo2  32927  prter2  33184  eqlkr2  33405  tendoidcl  35075  cdlemk56  35277  dihpN  35643  mapdhval  36031  hlhillcs  36268  isnacs3  36291  diophrw  36340  lzenom  36351  diophin  36354  pellexlem5  36415  pw2f1ocnv  36622  dnnumch2  36633  kelac2lem  36652  kelac2  36653  dfac21  36654  pwfi2f1o  36684  frlmpwfi  36686  mpaaeu  36739  rngunsnply  36762  mendbas  36773  mendplusgfval  36774  mendmulrfval  36776  mendsca  36778  mendvscafval  36779  subrgacs  36789  sdrgacs  36790  cntzsdrg  36791  idomodle  36793  proot1ex  36798  deg1mhm  36804  itgpowd  36819  trclubgNEW  36944  dmtrcl  36953  rntrcl  36954  brfvidRP  36999  trclrelexplem  37022  relexp01min  37024  trclimalb2  37037  dssmapfvd  37331  ntrk0kbimka  37357  ntrrn  37440  dssmapntrcls  37446  amgm2d  37523  amgm3d  37524  amgm4d  37525  hashnzfzclim  37543  ofsubid  37545  ofdivrec  37547  dvconstbi  37555  fzisoeu  38455  iuneqfzuzlem  38491  sumnnodd  38697  negcncfg  38766  cnfdmsn  38767  divcncf  38769  dvmptresicc  38809  itgcoscmulx  38861  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  stoweidlem42  38935  stoweidlem44  38937  stoweidlem48  38941  stoweidlem62  38955  stoweid  38956  stirlinglem7  38973  stirlinglem11  38977  stirlinglem12  38978  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem24  39024  fourierdlem48  39047  fourierdlem49  39048  fourierdlem62  39061  fourierdlem70  39069  fourierdlem80  39079  fourierdlem83  39082  fourierdlem85  39084  fourierdlem102  39101  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem114  39113  etransclem18  39145  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem35  39162  etransclem46  39173  ovolval5lem3  39544  iccpartipre  39959  iccpartiltu  39960  fmtnoprmfac2lem1  40016  mod42tp1mod8  40057  sfprmdvdsmersenne  40058  perfectALTVlem2  40165  stgoldbwt  40198  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem2  40222  mptmpt2opabbrd  40335  isusgrs  40386  isusgrop  40392  usgrop  40393  uspgr1ewop  40474  usgr2v1e2w  40478  uhgrspan1  40527  upgrres1  40532  umgrres1  40533  usgrres1  40534  isfusgrcl  40540  fusgredgfi  40544  usgr1v0e  40545  nbgrval  40560  nbusgrf1o1  40598  nbfusgrlevtxm2  40606  uvtxa01vtx0  40623  nbupgruvtxres  40634  usgrexi  40661  cusgrexi  40662  cusgrres  40664  cusgrfilem3  40673  sizusglecusg  40679  vtxdgfval  40683  vtxdgf  40686  vtxdlfgrval  40700  vtxd0nedgb  40703  vtxdusgr0edgnelALT  40711  1loopgrvd0  40719  1egrvtxdg1  40725  1egrvtxdg0  40727  p1evtxdeqlem  40728  p1evtxdeq  40729  p1evtxdp1  40730  umgr2v2eedg  40740  umgr2v2e  40741  vdiscusgrb  40746  vdegp1ai-av  40752  vdegp1bi-av  40753  ewlkle  40807  1wlksfval  40811  wlksfval  40812  1wlksv  40824  1wlk1ewlk  40844  uspgr2wlkeq  40854  1wlkp1lem8  40889  upgr2pthnlp  40938  1wlkiswwlks2  41072  wlksnwwlknvbij  41114  wwlksnextproplem1  41115  2pthdlem1  41137  elwwlks2  41170  clwlkclwwlklem1  41208  clwwlksnfi  41220  clwwlksvbij  41229  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  0wlkOnlem1  41286  0wlkOns1  41289  31wlkdlem4  41329  upgr3v3e3cycl  41347  trlsegvdeglem3  41390  trlsegvdeglem5  41392  eupth2lemb  41405  frgr3v  41445  frgr2wwlk1  41494  fusgreghash2wspv  41499  idmgmhm  41578  mgmplusgiopALT  41620  sgrp2sgrp  41654  isrnghm  41682  lidlmmgm  41715  2zrngnmlid  41739  dfrngc2  41764  rnghmsscmap2  41765  rnghmsscmap  41766  rngchomfvalALTV  41776  rngcidALTV  41783  funcrngcsetcALT  41791  dfringc2  41810  rhmsscmap2  41811  rhmsscmap  41812  rhmsscrnghm  41818  rngcresringcat  41822  funcringcsetcALTV2lem8  41835  ringchomfvalALTV  41839  ringcidALTV  41846  funcringcsetclem8ALTV  41858  srhmsubc  41868  fldc  41875  rngcrescrhm  41877  rhmsubclem3  41880  srhmsubcALTV  41887  fldcALTV  41894  rngcrescrhmALTV  41896  altgsumbcALT  41924  zlmodzxzel  41926  zlmodzxzsubm  41930  zlmodzxzsub  41931  gsumpr  41932  scmsuppss  41947  ply1mulgsum  41972  dmatALTbas  41984  lcoop  41994  lincval0  41998  lco0  42010  linds0  42048  snlindsntorlem  42053  lmod1lem2  42071  lmod1lem3  42072  lmod1zr  42076  lmod1zrnlvec  42077  zlmodzxznm  42080  zlmodzxzldeplem4  42086  expnegico01  42102  pw2m1lepw2m1  42104  fldivexpfllog2  42157  blennnelnn  42168  blenpw2  42170  nnpw2pmod  42175  blennnt2  42181  nnolog2flm1  42182  digfval  42189  dignnld  42195  dig2nn0ld  42196  0dig2nn0e  42204  0dig2nn0o  42205  amgmwlem  42357  amgmlemALT  42358  amgmw2d  42359