Theorem oveq2d 6034

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveq2d	⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq2 6026	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1397  (class class class)co 6018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  csbov1g  6059  caovassg  6181  caovdig  6197  caovdirg  6200  caov32d  6203  caov4d  6207  caov42d  6209  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  addasspig  7550  mulasspig  7552  distrpig  7553  dfplpq2  7574  mulpipq2  7591  addassnqg  7602  prarloclemarch  7638  prarloclemarch2  7639  ltrnqg  7640  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  nq0a0  7677  distrnq0  7679  addassnq0  7682  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  prarloclemcalc  7722  addnqprl  7749  addnqpru  7750  prmuloclemcalc  7785  mulnqprl  7788  mulnqpru  7789  distrlem4prl  7804  distrlem4pru  7805  1idprl  7810  1idpru  7811  ltexprlemloc  7827  addcanprleml  7834  addcanprlemu  7835  recexprlem1ssu  7854  ltmprr  7862  caucvgprlemcanl  7864  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexb  7927  caucvgprprlemaddq  7928  caucvgprprlem1  7929  addcmpblnr  7959  mulcmpblnrlemg  7960  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  ltsrprg  7967  recexgt0sr  7993  mulgt0sr  7998  caucvgsrlemgt1  8015  caucvgsrlemoffval  8016  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  suplocsr  8029  mulcnsr  8055  pitoregt0  8069  recidpirqlemcalc  8077  axmulcom  8091  axmulass  8093  axdistr  8094  ax0id  8098  axcnre  8101  recriota  8110  axcaucvglemcau  8118  axcaucvglemres  8119  mulrid  8176  adddirp1d  8206  mul32  8309  mul31  8310  add32  8338  add4  8340  add42  8341  cnegex  8357  addcan2  8360  addsubass  8389  subsub2  8407  nppcan2  8410  sub32  8413  nnncan  8414  sub4  8424  muladd  8563  subdi  8564  mul2neg  8577  submul2  8578  mulsub  8580  muls1d  8597  mulsubfacd  8598  add20  8654  recexre  8758  rereim  8766  apreap  8767  ltmul1  8772  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  mulap0  8834  divrecap  8868  divassap  8870  divmulasscomap  8876  divsubdirap  8888  divdivdivap  8893  divmul24ap  8896  divmuleqap  8897  divcanap6  8899  divdivap1  8903  divdivap2  8904  divsubdivap  8908  conjmulap  8909  div2negap  8915  apmul1  8968  cju  9141  nnmulcl  9164  add1p1  9394  sub1m1  9395  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  un0addcl  9435  un0mulcl  9436  zaddcllemneg  9518  qapne  9873  cnref1o  9885  rexsub  10088  xnegid  10094  xaddcom  10096  xnegdi  10103  xaddass  10104  xaddass2  10105  xpncan  10106  xnpcan  10107  xleadd1a  10108  xsubge0  10116  xposdif  10117  xlesubadd  10118  xadd4d  10120  lincmb01cmp  10238  iccf1o  10239  ige3m2fz  10284  fztp  10313  fzsuc2  10314  fseq1m1p1  10330  fzm1  10335  ige2m1fz1  10344  nn0split  10371  nnsplit  10372  fzo0addelr  10435  elfzoext  10438  fzval3  10450  zpnn0elfzo1  10454  fzosplitsnm1  10455  fzosplitpr  10480  fzosplitprm1  10481  fzoshftral  10485  rebtwn2zlemstep  10513  flhalf  10563  fldiv4lem1div2uz2  10567  modqval  10587  modqvalr  10588  modqdiffl  10598  modqfrac  10600  flqmod  10601  intqfrac  10602  zmod10  10603  modqmulnn  10605  modqvalp1  10606  modqid  10612  modqcyc  10622  modqcyc2  10623  modqmul1  10640  q2submod  10648  modqdi  10655  modqsubdir  10656  modqeqmodmin  10657  modsumfzodifsn  10659  addmodlteq  10661  frecuzrdgsuctlem  10686  uzsinds  10707  seqeq3  10715  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3m1  10736  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr2  10756  seqcaopr2g  10757  seq3caopr  10758  seqcaoprg  10759  seqf1oglem2a  10781  seqf1oglem2  10783  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  exp3vallem  10803  exp3val  10804  expp1  10809  expnegap0  10810  expineg2  10811  expn1ap0  10812  expm1t  10830  1exp  10831  expnegzap  10836  mulexpzap  10842  expadd  10844  expaddzaplem  10845  expaddzap  10846  expmul  10847  expmulzap  10848  m1expeven  10849  expsubap  10850  expp1zap  10851  expm1ap  10852  expdivap  10853  iexpcyc  10907  subsq2  10910  binom2  10914  binom21  10915  binom2sub  10916  binom2sub1  10917  mulbinom2  10919  binom3  10920  zesq  10921  bernneq  10923  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  nn0opthd  10985  facp1  10993  facnn2  10997  faclbnd  11004  faclbnd6  11007  bcval  11012  bccmpl  11017  bcn0  11018  bcnn  11020  bcnp1n  11022  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcp1m1  11028  bcpasc  11029  bcn2m1  11032  bcn2p1  11033  omgadd  11066  hashunlem  11068  hashunsng  11072  hashdifsn  11084  hashxp  11091  zfz1isolemsplit  11103  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  wrdf  11123  ccatfvalfi  11173  elfzelfzccat  11181  ccatlid  11187  ccatrid  11188  ccatass  11189  ccatalpha  11194  ccatws1leng  11215  ccats1val2  11221  ccatw2s1p1g  11226  swrdval  11233  swrd00g  11234  swrdf  11240  swrdfv2  11248  swrdwrdsymbg  11249  swrdspsleq  11252  swrds1  11253  swrdlsw  11254  ccatswrd  11255  swrdccat2  11256  pfxmpt  11265  pfxfv  11269  pfxeq  11281  pfxsuff1eqwrdeq  11284  ccatpfx  11286  pfxccat1  11287  swrdswrd  11290  pfxswrd  11291  swrdpfx  11292  pfxpfx  11293  pfxlswccat  11298  ccats1pfxeq  11299  ccats1pfxeqrex  11300  ccatopth2  11302  cats1un  11306  wrdind  11307  wrd2ind  11308  swrdccatfn  11309  swrdccatin1  11310  pfxccatin12lem4  11311  swrdccatin2  11314  pfxccatin12lem2c  11315  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat  11320  swrdccat3blem  11324  swrdccat3b  11325  swrdccatin2d  11329  pfxccatin12d  11330  reuccatpfxs1lem  11331  reuccatpfxs1  11332  shftcan1  11412  shftcan2  11413  cjval  11423  cjth  11424  crre  11435  replim  11437  remim  11438  reim0b  11440  rereb  11441  mulreap  11442  cjreb  11444  recj  11445  reneg  11446  readd  11447  resub  11448  remullem  11449  imcj  11453  imneg  11454  imadd  11455  imsub  11456  cjcj  11461  cjadd  11462  ipcnval  11464  cjmulrcl  11465  cjneg  11468  addcj  11469  cjsub  11470  cnrecnv  11488  caucvgrelemcau  11558  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniqlem  11572  resqrexlemover  11588  resqrexlemlo  11591  resqrexlemcalc1  11592  resqrexlemcalc3  11594  resqrexlemnm  11596  resqrexlemcvg  11597  absneg  11628  abscj  11630  sqabsadd  11633  sqabssub  11634  absmul  11647  absid  11649  absre  11655  absresq  11656  absexpzap  11658  recvalap  11675  abstri  11682  abs2dif2  11685  recan  11687  cau3lem  11692  amgm2  11696  bdtrilem  11817  xrmaxadd  11839  xrbdtri  11854  climaddc1  11907  climsubc1  11910  climcvg1nlem  11927  serf0  11930  fzf1o  11954  summodclem3  11959  summodclem2a  11960  summodc  11962  fsumsplitsn  11989  fsumm1  11995  fsumsplitsnun  11998  fsump1  11999  isummulc2  12005  fsumrev  12022  fisum0diag2  12026  fsummulc2  12027  fsumsub  12031  fsumabs  12044  telfsumo  12045  fsumparts  12049  fsumrelem  12050  fsumiun  12056  binomlem  12062  binom  12063  binom1p  12064  binom11  12065  binom1dif  12066  bcxmas  12068  isumsplit  12070  isum1p  12071  divcnv  12076  arisum2  12078  trireciplem  12079  trirecip  12080  geolim  12090  georeclim  12092  geo2sum  12093  geo2lim  12095  geoisum1c  12099  0.999...  12100  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratz  12111  mertenslem2  12115  mertensabs  12116  clim2prod  12118  prodfrecap  12125  prodfdivap  12126  prodmodclem3  12154  prodmodclem2a  12155  fprodm1  12177  fprodp1  12179  fprodunsn  12183  fprodfac  12194  fprodeq0  12196  fprodconst  12199  fprodrec  12208  fproddivap  12209  fprodsplitsn  12212  ege2le3  12250  efaddlem  12253  efsub  12260  efexp  12261  eftlub  12269  efsep  12270  effsumlt  12271  ef4p  12273  tanval3ap  12293  resinval  12294  recosval  12295  efi4p  12296  efival  12311  efmival  12312  efeul  12313  sinadd  12315  cosadd  12316  tanaddap  12318  sinsub  12319  cossub  12320  sincossq  12327  sin2t  12328  cos2t  12329  cos2tsin  12330  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  cos12dec  12347  absef  12349  absefib  12350  efieq1re  12351  demoivreALT  12353  eirraplem  12356  dvdsexp  12440  oexpneg  12456  opeo  12476  omeo  12477  m1exp1  12480  flodddiv4  12515  flodddiv4t2lthalf  12518  bitsval  12522  bitsp1  12530  bitsinv1lem  12540  bitsinv1  12541  divgcdnnr  12565  gcdaddm  12573  gcdadd  12574  gcdid  12575  modgcd  12580  gcdmultipled  12582  dvdsgcdidd  12583  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  bezoutlemex  12590  bezoutlembz  12593  absmulgcd  12606  gcdmultiple  12609  gcdmultiplez  12610  rpmulgcd  12615  rplpwr  12616  eucalginv  12646  eucalg  12649  lcmneg  12664  lcmgcdlem  12667  lcmgcd  12668  lcmid  12670  lcm1  12671  mulgcddvds  12684  qredeq  12686  divgcdcoprmex  12692  prmind2  12710  rpexp1i  12744  pw2dvdslemn  12755  pw2dvdseulemle  12757  pw2dvdseu  12758  oddpwdclemxy  12759  oddpwdclemdvds  12760  oddpwdclemndvds  12761  oddpwdclemdc  12763  2sqpwodd  12766  nn0gcdsq  12790  phiprmpw  12812  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  fermltl  12824  prmdiv  12825  hashgcdlem  12828  odzdvds  12836  vfermltl  12842  modprm0  12845  nnnn0modprm0  12846  modprmn0modprm0  12847  coprimeprodsq  12848  pythagtriplem1  12856  pythagtriplem4  12859  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  pythagtriplem18  12872  pythagtrip  12874  pcpremul  12884  pceu  12886  pczpre  12888  pcdiv  12893  pcqmul  12894  pcqdiv  12898  pcexp  12900  pcxqcl  12903  pczdvds  12905  pczndvds  12907  pczndvds2  12909  pcid  12915  pcneg  12916  pcdvdstr  12918  pcgcd1  12919  pcgcd  12920  pc2dvds  12921  pcaddlem  12930  pcadd  12931  pcadd2  12932  pcmpt  12934  pcmpt2  12935  fldivp1  12939  pcfac  12941  pcbc  12942  expnprm  12944  prmpwdvds  12946  pockthlem  12947  pockthi  12949  4sqlem7  12975  4sqlem9  12977  4sqlem10  12978  4sqlem2  12980  4sqlem3  12981  4sqlem4  12983  mul4sqlem  12984  4sqlem11  12992  4sqlem16  12997  4sqlem17  12998  4sqlem19  13000  setscomd  13141  ressvalsets  13165  strressid  13172  ressval3d  13173  ressinbasd  13175  ressressg  13176  ressabsg  13177  grpinvalem  13486  grpinva  13487  grprida  13488  isnsgrp  13507  sgrpass  13509  sgrp1  13512  sgrppropd  13514  prdssgrpd  13516  mnd32g  13528  mnd4g  13530  mndpropd  13541  prdsidlem  13548  prdsmndd  13549  imasmnd2  13553  mhmex  13563  mhmlin  13568  gsumwmhm  13599  grprcan  13638  grpsubval  13647  grpinvid2  13654  grpasscan2  13665  grpsubinv  13674  grpinvadd  13679  grpsubid1  13686  grpsubadd0sub  13688  grpsubadd  13689  grpsubsub  13690  grpaddsubass  13691  grppncan  13692  grpnnncan2  13698  grpsubpropd2  13706  imasgrp2  13715  mhmlem  13719  mhmid  13720  mhmmnd  13721  ghmgrp  13723  mulgnn0gsum  13733  mulgnnp1  13735  mulgaddcomlem  13750  mulgaddcom  13751  mulginvinv  13753  mulgnn0dir  13757  mulgdirlem  13758  mulgp1  13760  mulgneg2  13761  mulgnn0ass  13763  mulgass  13764  mulgmodid  13766  mulgsubdir  13767  nmzsubg  13815  0nsg  13819  eqger  13829  qussub  13842  ghmlin  13853  ghmsub  13856  conjghm  13881  ablsub4  13918  abladdsub4  13919  ablsubsub4  13924  ablsub32  13927  ablnnncan  13928  gsumfzmptfidmadd2  13945  gsumfzconst  13946  gsumfzmhm2  13949  gsumfzsnfd  13950  gsumsplit0  13951  mgpress  13963  rngass  13971  rngdi  13972  rngdir  13973  rngrz  13978  rngmneg2  13980  rngsubdi  13983  rngsubdir  13984  rngpropd  13987  imasrng  13988  srgass  14003  srgpcomp  14022  srgpcompp  14023  srgpcomppsc  14024  srg1expzeq1  14027  ringpropd  14070  ringrz  14076  ringnegr  14084  ringmneg2  14086  ringsubdi  14088  ringsubdir  14089  ring1  14091  imasring  14096  opprrng  14109  opprring  14111  mulgass3  14117  dvdsrd  14127  unitgrp  14149  invrfvald  14155  dvr1  14171  dvrass  14172  dvrcan1  14173  dvrcan3  14174  rdivmuldivd  14177  subrginv  14270  subrgdv  14271  resrhm2b  14282  islmod  14324  lmodlema  14325  islmodd  14326  lmodvs0  14355  lmodvneg1  14363  lmodvsubval2  14375  lmodsubvs  14376  lmodsubdi  14377  lmodsubdir  14378  lmodprop2d  14381  rmodislmodlem  14383  rmodislmod  14384  lsssn0  14403  sraval  14470  cnfldsub  14608  gsumfzfsumlem0  14619  gsumfzfsumlemm  14620  mulgrhm  14642  mulgrhm2  14643  znval  14669  znval2  14671  znunit  14692  psrval  14699  mplvalcoe  14723  mplval2g  14728  restabs  14918  cnprcl2k  14949  cnrest2r  14980  ispsmet  15066  psmettri2  15071  psmetsym  15072  ismet  15087  isxmet  15088  xmettri2  15104  xmetsym  15111  xmettri3  15117  mettri3  15118  xblss2ps  15147  xblss2  15148  comet  15242  xmetxp  15250  xmetxpbl  15251  txmetcnp  15261  fsumcncntop  15310  cncfi  15321  divcncfap  15357  limccl  15402  ellimc3apf  15403  limccnpcntop  15418  limccnp2lem  15419  reldvg  15422  dvfvalap  15424  eldvap  15425  dvcj  15452  dvfre  15453  dvexp  15454  dvexp2  15455  dvrecap  15456  dvmptaddx  15462  dvmptmulx  15463  dvmptnegcn  15465  dvmptsubcn  15466  dvmptcjx  15467  dvmptfsum  15468  dveflem  15469  dvef  15470  plyconst  15488  plyaddlem1  15490  plymullem1  15491  plyadd  15494  plymul  15495  plycoeid3  15500  plycolemc  15501  plyco  15502  plycjlemc  15503  plycj  15504  plyrecj  15506  dvply1  15508  dvply2g  15509  sin0pilem1  15524  sin0pilem2  15525  efper  15550  sinperlem  15551  efimpi  15562  ptolemy  15567  tangtx  15581  abssinper  15589  cosq34lt1  15593  rpcxpef  15637  rpcxpp1  15649  rpcxpneg  15650  rpcxpsub  15651  rpmulcxp  15652  rpdivcxp  15654  cxpmul  15655  rpcxpmul2  15656  rpcxproot  15657  cxpcom  15681  rpabscxpbnd  15683  rplogbval  15688  rplogbreexp  15696  rplogbzexp  15697  rprelogbmulexp  15699  rprelogbdiv  15700  relogbexpap  15701  rplogbcxp  15706  rpcxplogb  15707  logbgcd1irr  15710  logbgcd1irraplemap  15712  binom4  15722  wilthlem1  15723  sgmval  15726  sgmppw  15735  1sgmprm  15737  mersenne  15740  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgslem1  15748  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsval4  15768  lgsneg  15772  lgsneg1  15773  lgsmod  15774  lgsdir2  15781  lgsdirprm  15782  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgssq2  15789  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem2  15810  gausslemma2dlem3  15811  gausslemma2dlem4  15812  gausslemma2dlem5  15814  gausslemma2dlem6  15815  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  lgsquad2lem2  15830  lgsquad2  15831  lgsquad3  15832  m1lgs  15833  2lgslem3c  15843  2lgslem3d  15844  2lgslem3d1  15848  2sqlem2  15863  2sqlem3  15865  2sqlem4  15866  2sqlem8  15871  2sqlem9  15872  2sqlem10  15873  vtxdumgrfival  16168  p1evtxdeqfi  16182  p1evtxdp1fi  16183  iswlk  16193  upgr2wlkdc  16247  wlkres  16249  trlreslem  16259  isclwwlk  16264  clwwlkccatlem  16270  clwwlknp  16287  clwwlkn1  16288  clwwlkn2  16291  clwwlkext2edg  16292  clwwlknonex2lem1  16307  clwwlknonex2lem2  16308  clwwlknonex2  16309  iseupth  16317  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  depindlem1  16376  qdencn  16682  trilpolemclim  16691  trilpolemcl  16692  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  trilpo  16698  apdifflemf  16701  apdiff  16703  iswomni0  16707  redcwlpolemeq1  16710  redcwlpo  16711  nconstwlpolem0  16719  nconstwlpolemgt0  16720  nconstwlpo  16722  neapmkv  16724  gfsumval  16732  gsumgfsum1  16733  gsumgfsum  16736  gfsumsn  16737  gfsump1  16738  gfsumcl  16739