Theorem oveq1i 7416

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 7413	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Syntax hints:   = wceq 1542  (class class class)co 7406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  caov12  7632  caov411  7636  omopthlem1  8655  map1  9037  pw2eng  9075  fsuppunbi  9381  cnfcomlem  9691  cnfcom2  9694  infxpenc2  10014  adderpqlem  10946  addassnq  10950  distrnq  10953  halfnq  10968  archnq  10972  addclprlem2  11009  addcmpblnr  11061  ltsrpr  11069  m1m1sr  11085  recexsrlem  11095  sqgt0sr  11098  map2psrpr  11102  axi2m1  11151  axcnre  11156  mul02lem2  11388  addrid  11391  cnegex2  11393  addlid  11394  mvrraddi  11474  mvlladdi  11475  negsubdi  11513  mulneg1  11647  recextlem1  11841  recdiv  11917  divmul13i  11972  mvllmuli  12044  2p2e4  12344  2times  12345  1p2e3  12352  3p2e5  12360  3p3e6  12361  4p2e6  12362  4p3e7  12363  4p4e8  12364  5p2e7  12365  5p3e8  12366  5p4e9  12367  6p2e8  12368  6p3e9  12369  7p2e9  12370  1mhlfehlf  12428  8th4div3  12429  halfpm6th  12430  nneo  12643  9p1e10  12676  dfdec10  12677  num0h  12686  numsuc  12688  dec10p  12717  numma  12718  nummac  12719  numma2c  12720  numadd  12721  numaddc  12722  nummul2c  12724  decaddci  12735  decsubi  12737  5p5e10  12745  6p4e10  12746  7p3e10  12749  8p2e10  12754  decbin0  12814  decbin2  12815  xmulm1  13257  xadddi2  13273  x2times  13275  elfzp1b  13575  elfzm1b  13576  fz1ssfz0  13594  fz0to4untppr  13601  fz0sn0fz1  13615  fz0add1fz1  13699  elfz0lmr  13744  fldiv4p1lem1div2  13797  quoremz  13817  quoremnn0ALT  13819  uzrdgxfr  13929  mulexpz  14065  expaddz  14069  sqrecii  14144  sq4e2t8  14160  cu2  14161  i3  14164  iexpcyc  14168  binom2i  14173  binom3  14184  crreczi  14188  discr  14200  3dec  14223  nn0opthlem1  14225  nn0opth2i  14228  faclbnd  14247  bcp1nk  14274  bcpasc  14278  hashp1i  14360  hashxplem  14390  hashpw  14393  hashfun  14394  hashbc  14409  ccatlid  14533  pfxccatin12lem2c  14677  revs1  14712  cats1cat  14809  cats2cat  14810  lsws2  14852  lsws3  14853  lsws4  14854  s3s4  14881  s2s5  14882  s5s2  14883  imre  15052  crim  15059  remullem  15072  cnpart  15184  sqrtneglem  15210  absexpz  15249  absimle  15253  sqreulem  15303  amgm2  15313  iseraltlem2  15626  iseraltlem3  15627  modfsummod  15737  binomlem  15772  binom11  15775  arisum  15803  arisum2  15804  pwdif  15811  georeclim  15815  geo2sum  15816  mertenslem1  15827  mertens  15829  prodfrec  15838  fprodm1s  15911  fprodp1s  15912  fprodmodd  15938  fallfacfwd  15977  0risefac  15979  bpolydiflem  15995  bpoly2  15998  bpoly3  15999  bpoly4  16000  fsumcube  16001  efzval  16042  resinval  16075  recosval  16076  efi4p  16077  tan0  16091  efival  16092  sinhval  16094  coshval  16095  cosadd  16105  cos2tsin  16119  ef01bndlem  16124  cos1bnd  16127  cos2bnd  16128  absefib  16138  efieq1re  16139  demoivreALT  16141  eirrlem  16144  rpnnen2lem3  16156  rpnnen2lem11  16164  ruclem7  16176  3dvds  16271  3dvdsdec  16272  3dvds2dec  16273  odd2np1  16281  nn0o1gt2  16321  nn0o  16323  pwp1fsum  16331  divalglem2  16335  divalglem9  16341  flodddiv4  16353  m1bits  16378  sadcp1  16393  sadeq  16410  smupp1  16418  smumul  16431  gcdaddmlem  16462  3lcm2e6woprm  16549  nn0gcdsq  16685  phiprmpw  16706  prmdiv  16715  prmdiveq  16716  pythagtriplem1  16746  pythagtriplem12  16756  pythagtriplem14  16758  pockthi  16837  infpnlem1  16840  prmreclem4  16849  4sqlem12  16886  4sqlem13  16887  4sqlem19  16893  vdwapun  16904  vdwlem6  16916  0hashbc  16937  prmo2  16970  prmo3  16971  dec5dvds  16994  dec5nprm  16996  dec2nprm  16997  modxai  16998  modxp1i  17000  mod2xnegi  17001  modsubi  17002  gcdmodi  17004  decexp2  17005  decsplit0b  17010  decsplit1  17012  decsplit  17013  karatsuba  17014  2exp7  17018  2exp8  17019  3exp3  17022  5prm  17039  7prm  17041  11prm  17045  prmlem2  17050  37prm  17051  43prm  17052  83prm  17053  139prm  17054  163prm  17055  317prm  17056  631prm  17057  prmo5  17059  1259lem1  17061  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  2503lem1  17067  2503lem2  17068  2503lem3  17069  2503prm  17070  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  4001prm  17075  pwsbas  17430  rcaninv  17738  subsubc  17800  xpccatid  18137  subsubm  18694  smndex2dnrinv  18793  mulg2  18958  subsubg  19024  oppgmnd  19216  gsumwrev  19228  psgnunilem2  19358  sylow1lem1  19461  subgslw  19479  sylow3  19496  efginvrel2  19590  efgsfo  19602  frgpnabllem1  19736  gsumzaddlem  19784  gsummptfzsplitl  19796  gsummpt1n0  19828  dprdfid  19882  ablfac1lem  19933  pgpfac1lem3  19942  pgpfaclem1  19946  ablsimpgfindlem1  19972  mgpress  19997  mgpressOLD  19998  srgbinomlem4  20046  opprring  20154  unitsubm  20193  subsubrg  20383  cntzsdrg  20411  subdrgint  20412  lsslss  20565  xrsnsgrp  20974  gzrngunit  21004  expghm  21037  chrid  21071  zrhpsgnmhm  21129  psgndiflemA  21146  frlmip  21325  frlmphl  21328  evlsval  21641  mpff  21659  coe1fzgsumdlem  21817  evl1gsumdlem  21867  matvsca2  21922  mattposvs  21949  m2detleiblem3  22123  m2detleiblem4  22124  cpmidpmat  22367  resstopn  22682  cnmpt1res  23172  ressuss  23759  iscusp2  23799  ucnextcn  23801  txmetcnp  24048  rerest  24312  xrtgioo  24314  xrrest  24315  cnmpopc  24436  xrhmeo  24454  clmvs2  24602  clmnegneg  24612  ncvsm1  24663  ncvspi  24665  cphassir  24724  cphipval2  24750  reust  24890  rrxprds  24898  csbren  24908  rrxdsfi  24920  minveclem2  24935  ovolunlem1a  25005  ovolicc2lem4  25029  uniioombllem5  25096  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgmulc2  25343  limcres  25395  dvfval  25406  dvreslem  25418  dvres2lem  25419  dvcnp2  25429  cpnres  25446  dvcobr  25455  dveflem  25488  lhop1lem  25522  lhop2  25524  dvcnvrelem2  25527  plyun0  25703  coeeulem  25730  coeeu  25731  dvply1  25789  dvtaylp  25874  taylthlem2  25878  taylth  25879  dvradcnv  25925  pserdvlem2  25932  abelthlem8  25943  abelth  25945  sinhalfpilem  25965  cospi  25974  eulerid  25976  cos2pi  25978  ef2kpi  25980  sinhalfpip  25994  sinhalfpim  25995  coshalfpip  25996  coshalfpim  25997  sincosq3sgn  26002  sincosq4sgn  26003  tangtx  26007  sincos4thpi  26015  sincos6thpi  26017  sineq0  26025  tanregt0  26040  logm1  26089  abslogle  26118  tanarg  26119  logcnlem4  26145  advlogexp  26155  cxpsqrt  26203  dvsqrt  26240  dvcnsqrt  26242  cxpcn3  26246  root1cj  26254  cxpeq  26255  logb1  26264  2logb9irr  26290  sqrt2cxp2logb9e3  26294  ang180lem1  26304  ang180lem2  26305  ang180lem3  26306  lawcos  26311  isosctrlem1  26313  isosctrlem2  26314  quad2  26334  1cubrlem  26336  1cubr  26337  dcubic2  26339  mcubic  26342  binom4  26345  dquartlem1  26346  quart1lem  26350  quart1  26351  quartlem1  26352  asinlem  26363  asinlem2  26364  asinlem3a  26365  acosneg  26382  efiasin  26383  asinsinlem  26386  asinsin  26387  acoscos  26388  asin1  26389  acosbnd  26395  atancj  26405  efiatan  26407  atanlogaddlem  26408  efiatan2  26412  2efiatan  26413  tanatan  26414  cosatan  26416  atantan  26418  atanbndlem  26420  atans2  26426  dvatan  26430  atantayl  26432  atantayl2  26433  log2cnv  26439  log2tlbnd  26440  log2ublem2  26442  log2ublem3  26443  log2ub  26444  birthday  26449  jensenlem1  26481  amgmlem  26484  lgamgulmlem2  26524  lgamgulmlem5  26527  lgambdd  26531  ftalem2  26568  ftalem5  26571  ftalem6  26572  basellem2  26576  basellem3  26577  basellem5  26579  basellem8  26582  basellem9  26583  mule1  26642  ppi1i  26662  musum  26685  ppiublem1  26695  ppiub  26697  chtublem  26704  chtub  26705  dchrptlem1  26757  dchrptlem2  26758  bclbnd  26773  bposlem6  26782  bposlem8  26784  bposlem9  26785  lgsdir2lem1  26818  lgsdir2lem2  26819  lgsdir2lem4  26821  lgsdir2lem5  26822  lgsne0  26828  1lgs  26833  gausslemma2dlem0e  26853  gausslemma2dlem0f  26854  gausslemma2dlem3  26861  gausslemma2d  26867  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgseisenlem4  26871  lgseisen  26872  lgsquadlem1  26873  lgsquadlem2  26874  lgsquad2lem1  26877  lgsquad2lem2  26878  m1lgs  26881  2lgslem3a  26889  2lgslem3b  26890  2lgslem3c  26891  2lgslem3d  26892  2lgsoddprmlem3a  26903  2lgsoddprmlem3b  26904  2lgsoddprmlem3c  26905  2lgsoddprmlem3d  26906  addsqnreup  26936  chebbnd1lem2  26963  chebbnd1lem3  26964  rplogsumlem2  26978  dchrisum0flblem1  27001  dchrisum0re  27006  mulog2sumlem2  27028  chpdifbndlem1  27046  pntpbnd1a  27078  pntpbnd2  27080  pntibndlem2  27084  pntibndlem3  27085  pntlemg  27091  pntlemk  27099  pntlemo  27100  axsegconlem1  28165  ax5seglem7  28183  axlowdimlem3  28192  axlowdimlem16  28205  axlowdimlem17  28206  elntg2  28233  vdegp1bi  28784  vtxdginducedm1  28790  wlkp1lem1  28920  spthispth  28973  2wlkdlem1  29169  2pthd  29184  clwlkclwwlkfo  29252  3wlkdlem1  29402  3pthd  29417  eucrct2eupth  29488  numclwwlk5  29631  numclwwlk7  29634  frgrregord013  29638  ex-fl  29690  ex-mod  29692  ex-exp  29693  ex-bc  29695  ex-lcm  29701  ex-ind-dvds  29704  vc2OLD  29809  vc0  29815  vcm  29817  nvm1  29906  nvpi  29908  nvmtri  29912  nvge0  29914  ipval3  29950  ipidsq  29951  ip0i  30066  ip1ilem  30067  ip2i  30069  ipdirilem  30070  ipasslem10  30080  siilem1  30092  siii  30094  minvecolem2  30116  hvsubid  30267  hvaddsubval  30274  hvmul2negi  30289  hvadd12i  30298  hv2times  30302  hvnegdii  30303  hvaddcani  30306  hi01  30337  hisubcomi  30345  normlem0  30350  normlem1  30351  normlem3  30353  normlem9  30359  bcseqi  30361  normsqi  30373  norm-ii-i  30378  normsubi  30382  norm3difi  30388  norm3adifii  30389  normpar2i  30397  polid2i  30398  polidi  30399  chdmm2i  30719  chj12i  30763  spanunsni  30820  qlaxr5i  30876  osumcor2i  30885  spansnji  30887  pjadjii  30915  pjinormii  30917  pjsslem  30920  pjpythi  30963  mayete3i  30969  mayetes3i  30970  hoadd12i  31018  honegneg  31047  ho2times  31060  hoaddsubi  31062  hosd1i  31063  hosd2i  31064  honpncani  31068  lnopeq0lem1  31246  lnopunilem1  31251  lnophmlem2  31258  lnfn0i  31283  nmopcoadji  31342  nmopcoadj2i  31343  opsqrlem1  31381  opsqrlem5  31385  opsqrlem6  31386  pjclem3  31438  stadd3i  31489  mddmd2  31550  mdexchi  31576  cvexchlem  31609  atomli  31623  atordi  31625  atabs2i  31643  mdsymlem1  31644  iuninc  31780  suppss2f  31851  mptiffisupp  31903  suppss3  31937  dfdec100  32024  dpfrac1  32046  decdiv10  32050  dpmul100  32051  dp3mul10  32052  dpmul1000  32053  dpexpp1  32062  dpadd2  32064  dpadd  32065  dpmul  32067  dpmul4  32068  threehalves  32069  1mhdrd  32070  pfxlsw2ccat  32104  cyc2fv1  32268  cyc2fv2  32269  cycpmco2lem4  32276  cycpmco2lem5  32277  cyc3fv1  32284  cyc3fv2  32285  cyc3fv3  32286  archirngz  32323  gsumvsca2  32360  nn0omnd  32449  nn0archi  32451  xrge0slmod  32452  opprabs  32585  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  algextdeglem1  32761  lmatfvlem  32784  sqsscirc1  32877  cnvordtrestixx  32882  raddcn  32898  xrge0iifhom  32906  xrge0mulc1cn  32910  xrge0tmd  32914  lmlimxrge0  32917  qqhucn  32961  rrhcn  32966  qqtopn  32980  rrhqima  32983  brfae  33235  inelcarsg  33299  cndprobnul  33425  isrrvv  33431  ballotlem1  33474  ballotlem2  33476  ballotlemi1  33490  ballotlemii  33491  ballotlemic  33494  ballotlem1c  33495  ballotlemfrceq  33516  ballotth  33525  ofcs2  33545  signsvtn0  33570  signstfveq0  33577  signsvtp  33583  signsvtn  33584  signsvfpn  33585  signsvfnn  33586  signshf  33588  hashreprin  33621  reprfz1  33625  chtvalz  33630  breprexp  33634  breprexpnat  33635  hgt750lemd  33649  hgt750lem  33652  hgt750lem2  33653  subfacp1lem1  34159  subfacp1lem5  34164  subfacp1lem6  34165  subfaclim  34168  cvmliftlem5  34269  cvmliftlem8  34272  cvmliftlem10  34274  cvmliftlem13  34276  cvmlift2lem6  34288  cvmlift2lem12  34294  problem1  34639  problem2  34640  problem4  34642  quad3  34644  iexpire  34694  gg-dvcnp2  35163  gg-dvmulbr  35164  gg-dvcobr  35165  sin2h  36467  poimirlem16  36493  poimirlem17  36494  poimirlem18  36495  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem22  36499  poimirlem26  36503  mblfinlem3  36516  ismblfin  36518  itg2addnclem3  36530  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nc  36545  ftc1cnnc  36549  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  dvasin  36561  fdc  36602  heiborlem4  36671  heiborlem6  36673  dalem24  38557  pmod2iN  38709  cdleme9  39113  cdleme20aN  39169  cdleme22e  39204  cdleme22eALTN  39205  cdleme25cv  39218  cdleme29b  39235  cdlemh1  39675  cdlemh2  39676  cdlemk35  39772  cdlemkid1  39782  12gcd5e1  40857  60gcd7e1  40859  420gcd8e4  40860  12lcm5e60  40862  420lcm8e840  40865  lcm1un  40867  lcm2un  40868  lcm3un  40869  lcm4un  40870  lcm5un  40871  lcm6un  40872  lcm7un  40873  lcm8un  40874  3factsumint1  40875  3factsumint3  40877  lcmineqlem10  40892  3exp7  40907  3lexlogpow5ineq1  40908  3lexlogpow5ineq5  40914  aks4d1p1  40930  5bc2eq10  40947  2ap1caineq  40950  mhphf2  41168  sqmid3api  41193  sqn5i  41195  sqdeccom12  41199  235t711  41201  nn0expgcd  41222  re1m1e0m0  41267  readdlid  41273  remul02  41275  sn-1ticom  41304  sn-mullid  41305  sn-0tie0  41309  sn-mul02  41310  sn-inelr  41335  flt4lem5e  41395  pellexlem5  41557  reglog1  41620  jm2.23  41721  jm2.27c  41732  lnmlsslnm  41809  lmhmlnmsplit  41815  areaquad  41951  oaomoencom  42053  resqrtvalex  42382  imsqrtvalex  42383  cotrclrcl  42479  inductionexd  42892  hashnzfz2  43066  lhe4.4ex1a  43074  binomcxplemdvsum  43100  binomcxplemnotnn0  43101  binomcxp  43102  sineq0ALT  43684  unirnmapsn  43899  fzisoeu  43997  fsummulc1f  44274  fprodexp  44297  constlimc  44327  sumnnodd  44333  limcresiooub  44345  limcresioolb  44346  cncfshiftioo  44595  fperdvper  44622  dvnmul  44646  dvmptfprod  44648  itgsinexplem1  44657  stoweidlem11  44714  stoweidlem13  44716  stoweidlem26  44729  stoweidlem34  44737  wallispilem4  44771  wallispi2lem1  44774  wallispi2lem2  44775  stirlinglem11  44787  dirkerper  44799  dirkertrigeqlem1  44801  dirkertrigeqlem3  44803  dirkercncflem1  44806  dirkercncflem4  44809  fourierdlem30  44840  fourierdlem32  44842  fourierdlem33  44843  fourierdlem42  44852  fourierdlem46  44855  fourierdlem47  44856  fourierdlem57  44866  fourierdlem60  44869  fourierdlem61  44870  fourierdlem62  44871  fourierdlem68  44877  fourierdlem73  44882  fourierdlem79  44888  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem96  44905  fourierdlem97  44906  fourierdlem98  44907  fourierdlem99  44908  fourierdlem100  44909  fourierdlem103  44912  fourierdlem104  44913  fourierdlem108  44917  fourierdlem110  44919  fourierdlem113  44922  sqwvfoura  44931  sqwvfourb  44932  fourierswlem  44933  fouriersw  44934  fouriercn  44935  etransclem4  44941  etransclem7  44944  etransclem23  44960  etransclem24  44961  etransclem25  44962  etransclem26  44963  etransclem31  44968  etransclem32  44969  etransclem35  44972  etransclem37  44974  etransclem46  44983  rrndistlt  44993  sge0tsms  45083  sge0xaddlem2  45137  vonioolem2  45384  natlocalincr  45577  upwordsing  45585  tworepnotupword  45587  1t10e1p1e11  46005  deccarry  46006  1fzopredsuc  46019  m1mod0mod1  46024  iccpartgt  46082  fmtno0  46195  fmtno1  46196  fmtnorec2  46198  fmtno2  46205  fmtno3  46206  fmtno4  46207  fmtno5  46212  257prm  46216  fmtnofac1  46225  fmtno4prmfac  46227  fmtno4prmfac193  46228  fmtno4nprmfac193  46229  m2prm  46246  m3prm  46247  flsqrt5  46249  3ndvds4  46250  139prmALT  46251  31prm  46252  127prm  46254  m11nprm  46256  lighneallem2  46261  lighneallem3  46262  3exp4mod41  46271  41prothprmlem1  46272  41prothprmlem2  46273  41prothprm  46274  m1expevenALTV  46302  1oddALTV  46345  6even  46366  8even  46368  2exp340mod341  46388  341fppr2  46389  4fppr1  46390  8exp8mod9  46391  9fppr8  46392  nfermltl8rev  46397  gbpart7  46422  gbpart9  46424  gbpart11  46425  sbgoldbo  46442  bgoldbtbndlem1  46460  tgoldbachlt  46471  subsubmgm  46554  opprrng  46661  subsubrng  46727  altgsumbcALT  46983  lincfsuppcl  47048  linccl  47049  lincvalsn  47052  lincdifsn  47059  lincsum  47064  lincscm  47065  lindslinindimp2lem4  47096  lindslinindsimp2lem5  47097  snlindsntor  47106  lincresunit3lem2  47115  zlmodzxzldeplem3  47137  ldepsnlinc  47143  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  ackval2  47322  ackval2012  47331  ackval3012  47332  ackval41a  47334  ackval42  47336  ackval42a  47337  affinecomb1  47342  rrx2linest  47382  itschlc0yqe  47400  itsclc0yqsollem1  47402  itscnhlc0xyqsol  47405  itschlc0xyqsol1  47406  itsclquadb  47416  2itscplem2  47419  itscnhlinecirc02plem2  47423  sinh-conventional  47738  onetansqsecsq  47760  cotsqcscsq  47761  mvlraddi  47771  mvrladdi  47772  mvlrmuli  47778  amgmwlem  47803  amgmlemALT  47804