Theorem oveq1i 7166

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq1i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq1 7163	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Syntax hints:   = wceq 1537  (class class class)co 7156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  caov12  7376  caov411  7380  omopthlem1  8282  map1  8592  pw2eng  8623  fsuppunbi  8854  cnfcomlem  9162  cnfcom2  9165  infxpenc2  9448  adderpqlem  10376  addassnq  10380  distrnq  10383  halfnq  10398  archnq  10402  addclprlem2  10439  addcmpblnr  10491  ltsrpr  10499  m1m1sr  10515  recexsrlem  10525  sqgt0sr  10528  map2psrpr  10532  axi2m1  10581  axcnre  10586  mul02lem2  10817  addid1  10820  cnegex2  10822  addid2  10823  mvrraddi  10903  mvlladdi  10904  negsubdi  10942  mulneg1  11076  recextlem1  11270  recdiv  11346  divmul13i  11401  mvllmuli  11473  2p2e4  11773  2times  11774  1p2e3  11781  3p2e5  11789  3p3e6  11790  4p2e6  11791  4p3e7  11792  4p4e8  11793  5p2e7  11794  5p3e8  11795  5p4e9  11796  6p2e8  11797  6p3e9  11798  7p2e9  11799  1mhlfehlf  11857  8th4div3  11858  halfpm6th  11859  nneo  12067  9p1e10  12101  dfdec10  12102  num0h  12111  numsuc  12113  dec10p  12142  numma  12143  nummac  12144  numma2c  12145  numadd  12146  numaddc  12147  nummul2c  12149  decaddci  12160  decsubi  12162  5p5e10  12170  6p4e10  12171  7p3e10  12174  8p2e10  12179  decbin0  12239  decbin2  12240  xmulm1  12675  xadddi2  12691  x2times  12693  elfzp1b  12985  elfzm1b  12986  fz1ssfz0  13004  fz0to4untppr  13011  fz0sn0fz1  13025  fz0add1fz1  13108  elfz0lmr  13153  fldiv4p1lem1div2  13206  quoremz  13224  quoremnn0ALT  13226  uzrdgxfr  13336  mulexpz  13470  expaddz  13474  sqrecii  13547  sq4e2t8  13563  cu2  13564  i3  13567  iexpcyc  13570  binom2i  13575  binom3  13586  crreczi  13590  discr  13602  3dec  13627  nn0opthlem1  13629  nn0opth2i  13632  faclbnd  13651  bcp1nk  13678  bcpasc  13682  hashp1i  13765  hashxplem  13795  hashpw  13798  hashfun  13799  hashbc  13812  ccatlid  13940  pfxccatin12lem2c  14092  revs1  14127  cats1cat  14223  cats2cat  14224  lsws2  14266  lsws3  14267  lsws4  14268  s3s4  14295  s2s5  14296  s5s2  14297  imre  14467  crim  14474  remullem  14487  cnpart  14599  sqrtneglem  14626  absexpz  14665  absimle  14669  sqreulem  14719  amgm2  14729  iseraltlem2  15039  iseraltlem3  15040  modfsummod  15149  binomlem  15184  binom11  15187  arisum  15215  arisum2  15216  pwdif  15223  georeclim  15228  geo2sum  15229  mertenslem1  15240  mertens  15242  prodfrec  15251  fprodm1s  15324  fprodp1s  15325  fprodmodd  15351  fallfacfwd  15390  0risefac  15392  bpolydiflem  15408  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  efzval  15455  resinval  15488  recosval  15489  efi4p  15490  tan0  15504  efival  15505  sinhval  15507  coshval  15508  cosadd  15518  cos2tsin  15532  ef01bndlem  15537  cos1bnd  15540  cos2bnd  15541  absefib  15551  efieq1re  15552  demoivreALT  15554  eirrlem  15557  rpnnen2lem3  15569  rpnnen2lem11  15577  ruclem7  15589  3dvds  15680  3dvdsdec  15681  3dvds2dec  15682  odd2np1  15690  nn0o1gt2  15732  nn0o  15734  pwp1fsum  15742  divalglem2  15746  divalglem9  15752  flodddiv4  15764  m1bits  15789  sadcp1  15804  sadeq  15821  smupp1  15829  smumul  15842  gcdaddmlem  15872  3lcm2e6woprm  15959  nn0gcdsq  16092  phiprmpw  16113  prmdiv  16122  prmdiveq  16123  pythagtriplem1  16153  pythagtriplem12  16163  pythagtriplem14  16165  pockthi  16243  infpnlem1  16246  prmreclem4  16255  4sqlem12  16292  4sqlem13  16293  4sqlem19  16299  vdwapun  16310  vdwlem6  16322  0hashbc  16343  prmo2  16376  prmo3  16377  dec5dvds  16400  dec5nprm  16402  dec2nprm  16403  modxai  16404  modxp1i  16406  mod2xnegi  16407  modsubi  16408  gcdmodi  16410  decexp2  16411  decsplit0b  16416  decsplit1  16418  decsplit  16419  karatsuba  16420  2exp8  16423  3exp3  16425  5prm  16442  7prm  16444  11prm  16448  prmlem2  16453  37prm  16454  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  prmo5  16462  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  pwsbas  16760  rcaninv  17064  subsubc  17123  xpccatid  17438  subsubm  17981  smndex2dnrinv  18080  mulg2  18237  subsubg  18302  oppgmnd  18482  gsumwrev  18494  psgnunilem2  18623  sylow1lem1  18723  subgslw  18741  sylow3  18758  efginvrel2  18853  efgsfo  18865  frgpnabllem1  18993  gsumzaddlem  19041  gsummptfzsplitl  19053  gsummpt1n0  19085  dprdfid  19139  ablfac1lem  19190  pgpfac1lem3  19199  pgpfaclem1  19203  ablsimpgfindlem1  19229  mgpress  19250  srgbinomlem4  19293  opprring  19381  unitsubm  19420  subsubrg  19561  cntzsdrg  19581  subdrgint  19582  lsslss  19733  evlsval  20299  mpff  20317  coe1fzgsumdlem  20469  evl1gsumdlem  20519  xrsnsgrp  20581  gzrngunit  20611  expghm  20643  chrid  20674  zrhpsgnmhm  20728  psgndiflemA  20745  frlmip  20922  frlmphl  20925  matvsca2  21037  mattposvs  21064  m2detleiblem3  21238  m2detleiblem4  21239  cpmidpmat  21481  resstopn  21794  cnmpt1res  22284  ressuss  22872  iscusp2  22911  ucnextcn  22913  txmetcnp  23157  rerest  23412  xrtgioo  23414  xrrest  23415  cnmpopc  23532  xrhmeo  23550  clmvs2  23698  clmnegneg  23708  ncvsm1  23758  ncvspi  23760  cphassir  23819  cphipval2  23844  reust  23984  rrxprds  23992  csbren  24002  rrxdsfi  24014  minveclem2  24029  ovolunlem1a  24097  ovolicc2lem4  24121  uniioombllem5  24188  iblabs  24429  iblabsr  24430  iblmulc2  24431  itgmulc2  24434  limcres  24484  dvfval  24495  dvreslem  24507  dvres2lem  24508  dvcnp2  24517  cpnres  24534  dvcobr  24543  dveflem  24576  lhop1lem  24610  lhop2  24612  dvcnvrelem2  24615  plyun0  24787  coeeulem  24814  coeeu  24815  dvply1  24873  dvtaylp  24958  taylthlem2  24962  taylth  24963  dvradcnv  25009  pserdvlem2  25016  abelthlem8  25027  abelth  25029  sinhalfpilem  25049  cospi  25058  eulerid  25060  cos2pi  25062  ef2kpi  25064  sinhalfpip  25078  sinhalfpim  25079  coshalfpip  25080  coshalfpim  25081  sincosq3sgn  25086  sincosq4sgn  25087  tangtx  25091  sincos4thpi  25099  sincos6thpi  25101  sineq0  25109  tanregt0  25123  logm1  25172  abslogle  25201  tanarg  25202  logcnlem4  25228  advlogexp  25238  cxpsqrt  25286  dvsqrt  25323  dvcnsqrt  25325  cxpcn3  25329  root1cj  25337  cxpeq  25338  logb1  25347  2logb9irr  25373  sqrt2cxp2logb9e3  25377  ang180lem1  25387  ang180lem2  25388  ang180lem3  25389  lawcos  25394  isosctrlem1  25396  isosctrlem2  25397  quad2  25417  1cubrlem  25419  1cubr  25420  dcubic2  25422  mcubic  25425  binom4  25428  dquartlem1  25429  quart1lem  25433  quart1  25434  quartlem1  25435  asinlem  25446  asinlem2  25447  asinlem3a  25448  acosneg  25465  efiasin  25466  asinsinlem  25469  asinsin  25470  acoscos  25471  asin1  25472  acosbnd  25478  atancj  25488  efiatan  25490  atanlogaddlem  25491  efiatan2  25495  2efiatan  25496  tanatan  25497  cosatan  25499  atantan  25501  atanbndlem  25503  atans2  25509  dvatan  25513  atantayl  25515  atantayl2  25516  log2cnv  25522  log2tlbnd  25523  log2ublem2  25525  log2ublem3  25526  log2ub  25527  birthday  25532  jensenlem1  25564  amgmlem  25567  lgamgulmlem2  25607  lgamgulmlem5  25610  lgambdd  25614  ftalem2  25651  ftalem5  25654  ftalem6  25655  basellem2  25659  basellem3  25660  basellem5  25662  basellem8  25665  basellem9  25666  mule1  25725  ppi1i  25745  musum  25768  ppiublem1  25778  ppiub  25780  chtublem  25787  chtub  25788  dchrptlem1  25840  dchrptlem2  25841  bclbnd  25856  bposlem6  25865  bposlem8  25867  bposlem9  25868  lgsdir2lem1  25901  lgsdir2lem2  25902  lgsdir2lem4  25904  lgsdir2lem5  25905  lgsne0  25911  1lgs  25916  gausslemma2dlem0e  25936  gausslemma2dlem0f  25937  gausslemma2dlem3  25944  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem1  25960  lgsquad2lem2  25961  m1lgs  25964  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgsoddprmlem3a  25986  2lgsoddprmlem3b  25987  2lgsoddprmlem3c  25988  2lgsoddprmlem3d  25989  addsqnreup  26019  chebbnd1lem2  26046  chebbnd1lem3  26047  rplogsumlem2  26061  dchrisum0flblem1  26084  dchrisum0re  26089  mulog2sumlem2  26111  chpdifbndlem1  26129  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntibndlem3  26168  pntlemg  26174  pntlemk  26182  pntlemo  26183  axsegconlem1  26703  ax5seglem7  26721  axlowdimlem3  26730  axlowdimlem16  26743  axlowdimlem17  26744  elntg2  26771  vdegp1bi  27319  vtxdginducedm1  27325  wlkp1lem1  27455  spthispth  27507  2wlkdlem1  27704  2pthd  27719  clwlkclwwlkfo  27787  3wlkdlem1  27938  3pthd  27953  eucrct2eupth  28024  numclwwlk5  28167  numclwwlk7  28170  frgrregord013  28174  ex-fl  28226  ex-mod  28228  ex-exp  28229  ex-bc  28231  ex-lcm  28237  ex-ind-dvds  28240  vc2OLD  28345  vc0  28351  vcm  28353  nvm1  28442  nvpi  28444  nvmtri  28448  nvge0  28450  ipval3  28486  ipidsq  28487  ip0i  28602  ip1ilem  28603  ip2i  28605  ipdirilem  28606  ipasslem10  28616  siilem1  28628  siii  28630  minvecolem2  28652  hvsubid  28803  hvaddsubval  28810  hvmul2negi  28825  hvadd12i  28834  hv2times  28838  hvnegdii  28839  hvaddcani  28842  hi01  28873  hisubcomi  28881  normlem0  28886  normlem1  28887  normlem3  28889  normlem9  28895  bcseqi  28897  normsqi  28909  norm-ii-i  28914  normsubi  28918  norm3difi  28924  norm3adifii  28925  normpar2i  28933  polid2i  28934  polidi  28935  chdmm2i  29255  chj12i  29299  spanunsni  29356  qlaxr5i  29412  osumcor2i  29421  spansnji  29423  pjadjii  29451  pjinormii  29453  pjsslem  29456  pjpythi  29499  mayete3i  29505  mayetes3i  29506  hoadd12i  29554  honegneg  29583  ho2times  29596  hoaddsubi  29598  hosd1i  29599  hosd2i  29600  honpncani  29604  lnopeq0lem1  29782  lnopunilem1  29787  lnophmlem2  29794  lnfn0i  29819  nmopcoadji  29878  nmopcoadj2i  29879  opsqrlem1  29917  opsqrlem5  29921  opsqrlem6  29922  pjclem3  29974  stadd3i  30025  mddmd2  30086  mdexchi  30112  cvexchlem  30145  atomli  30159  atordi  30161  atabs2i  30179  mdsymlem1  30180  iuninc  30312  suppss2f  30384  suppss3  30460  dfdec100  30546  dpfrac1  30568  decdiv10  30572  dpmul100  30573  dp3mul10  30574  dpmul1000  30575  dpexpp1  30584  dpadd2  30586  dpadd  30587  dpmul  30589  dpmul4  30590  threehalves  30591  1mhdrd  30592  pfxlsw2ccat  30626  cyc2fv1  30763  cyc2fv2  30764  cycpmco2lem4  30771  cycpmco2lem5  30772  cyc3fv1  30779  cyc3fv2  30780  cyc3fv3  30781  archirngz  30818  gsumvsca2  30855  nn0omnd  30914  nn0archi  30916  xrge0slmod  30917  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  lmatfvlem  31080  sqsscirc1  31151  cnvordtrestixx  31156  raddcn  31172  xrge0iifhom  31180  xrge0mulc1cn  31184  xrge0tmd  31188  lmlimxrge0  31191  qqhucn  31233  rrhcn  31238  qqtopn  31252  rrhqima  31255  brfae  31507  inelcarsg  31569  cndprobnul  31695  isrrvv  31701  ballotlem1  31744  ballotlem2  31746  ballotlemi1  31760  ballotlemii  31761  ballotlemic  31764  ballotlem1c  31765  ballotlemfrceq  31786  ballotth  31795  ofcs2  31815  signsvtn0  31840  signstfveq0  31847  signsvtp  31853  signsvtn  31854  signsvfpn  31855  signsvfnn  31856  signshf  31858  hashreprin  31891  reprfz1  31895  chtvalz  31900  breprexp  31904  breprexpnat  31905  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  subfacp1lem1  32426  subfacp1lem5  32431  subfacp1lem6  32432  subfaclim  32435  cvmliftlem5  32536  cvmliftlem8  32539  cvmliftlem10  32541  cvmliftlem13  32543  cvmlift2lem6  32555  cvmlift2lem12  32561  problem1  32908  problem2  32909  problem4  32911  quad3  32913  iexpire  32967  sin2h  34897  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem26  34933  mblfinlem3  34946  ismblfin  34948  itg2addnclem3  34960  iblabsnc  34971  iblmulc2nc  34972  itgmulc2nc  34975  ftc1cnnc  34981  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  dvasin  34993  fdc  35035  heiborlem4  35107  heiborlem6  35109  dalem24  36848  pmod2iN  37000  cdleme9  37404  cdleme20aN  37460  cdleme22e  37495  cdleme22eALTN  37496  cdleme25cv  37509  cdleme29b  37526  cdlemh1  37966  cdlemh2  37967  cdlemk35  38063  cdlemkid1  38073  12gcd5e1  39124  60gcd7e1  39126  420gcd8e4  39127  12lcm5e60  39129  420lcm8e840  39132  lcm1un  39134  lcm2un  39135  lcm3un  39136  lcm4un  39137  lcm5un  39138  lcm6un  39139  lcm7un  39140  lcm8un  39141  sqmid3api  39218  sqn5i  39220  sqdeccom12  39224  235t711  39226  nn0expgcd  39233  re1m1e0m0  39276  readdid2  39282  remul02  39284  pellexlem5  39479  reglog1  39542  jm2.23  39642  jm2.27c  39653  lnmlsslnm  39730  lmhmlnmsplit  39736  areaquad  39872  cotrclrcl  40136  inductionexd  40554  hashnzfz2  40702  lhe4.4ex1a  40710  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  binomcxp  40738  sineq0ALT  41320  unirnmapsn  41526  fzisoeu  41616  fsummulc1f  41900  fprodexp  41924  constlimc  41954  sumnnodd  41960  limcresiooub  41972  limcresioolb  41973  cncfshiftioo  42224  fperdvper  42252  dvnmul  42277  dvmptfprod  42279  itgsinexplem1  42288  stoweidlem11  42345  stoweidlem13  42347  stoweidlem26  42360  stoweidlem34  42368  wallispilem4  42402  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem11  42418  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem3  42434  dirkercncflem1  42437  dirkercncflem4  42440  fourierdlem30  42471  fourierdlem32  42473  fourierdlem33  42474  fourierdlem42  42483  fourierdlem46  42486  fourierdlem47  42487  fourierdlem57  42497  fourierdlem60  42500  fourierdlem61  42501  fourierdlem62  42502  fourierdlem68  42508  fourierdlem73  42513  fourierdlem79  42519  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem100  42540  fourierdlem103  42543  fourierdlem104  42544  fourierdlem108  42548  fourierdlem110  42550  fourierdlem113  42553  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  fouriercn  42566  etransclem4  42572  etransclem7  42575  etransclem23  42591  etransclem24  42592  etransclem25  42593  etransclem26  42594  etransclem31  42599  etransclem32  42600  etransclem35  42603  etransclem37  42605  etransclem46  42614  rrndistlt  42624  sge0tsms  42711  sge0xaddlem2  42765  vonioolem2  43012  1t10e1p1e11  43559  deccarry  43560  1fzopredsuc  43573  m1mod0mod1  43578  iccpartgt  43636  fmtno0  43751  fmtno1  43752  fmtnorec2  43754  fmtno2  43761  fmtno3  43762  fmtno4  43763  fmtno5  43768  257prm  43772  fmtnofac1  43781  fmtno4prmfac  43783  fmtno4prmfac193  43784  fmtno4nprmfac193  43785  m2prm  43802  m3prm  43803  flsqrt5  43806  3ndvds4  43807  139prmALT  43808  31prm  43809  2exp7  43811  127prm  43812  m11nprm  43815  lighneallem2  43820  lighneallem3  43821  3exp4mod41  43830  41prothprmlem1  43831  41prothprmlem2  43832  41prothprm  43833  m1expevenALTV  43861  1oddALTV  43904  6even  43925  8even  43927  2exp340mod341  43947  341fppr2  43948  4fppr1  43949  8exp8mod9  43950  9fppr8  43951  nfermltl8rev  43956  gbpart7  43981  gbpart9  43983  gbpart11  43984  sbgoldbo  44001  bgoldbtbndlem1  44019  tgoldbachlt  44030  subsubmgm  44113  altgsumbcALT  44450  lincfsuppcl  44517  linccl  44518  lincvalsn  44521  lincdifsn  44528  lincsum  44533  lincscm  44534  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  snlindsntor  44575  lincresunit3lem2  44584  zlmodzxzldeplem3  44606  ldepsnlinc  44612  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  affinecomb1  44738  rrx2linest  44778  itschlc0yqe  44796  itsclc0yqsollem1  44798  itscnhlc0xyqsol  44801  itschlc0xyqsol1  44802  itsclquadb  44812  2itscplem2  44815  itscnhlinecirc02plem2  44819  sinh-conventional  44887  onetansqsecsq  44909  cotsqcscsq  44910  mvlraddi  44920  mvrladdi  44921  mvlrmuli  44927  amgmwlem  44952  amgmlemALT  44953