Theorem oveq2d 6044

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 6036	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6028

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  csbov1g  6069  caovassg  6191  caovdig  6207  caovdirg  6210  caov32d  6213  caov4d  6217  caov42d  6219  suppofss1dcl  6442  suppofss2dcl  6443  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  addasspig  7593  mulasspig  7595  distrpig  7596  dfplpq2  7617  mulpipq2  7634  addassnqg  7645  prarloclemarch  7681  prarloclemarch2  7682  ltrnqg  7683  enq0sym  7695  addnq0mo  7710  mulnq0mo  7711  addnnnq0  7712  nq0a0  7720  distrnq0  7722  addassnq0  7725  prarloclemlo  7757  prarloclem3  7760  prarloclem5  7763  prarloclemcalc  7765  addnqprl  7792  addnqpru  7793  prmuloclemcalc  7828  mulnqprl  7831  mulnqpru  7832  distrlem4prl  7847  distrlem4pru  7848  1idprl  7853  1idpru  7854  ltexprlemloc  7870  addcanprleml  7877  addcanprlemu  7878  recexprlem1ssu  7897  ltmprr  7905  caucvgprlemcanl  7907  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlemlim  7924  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkeqj  7953  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexb  7970  caucvgprprlemaddq  7971  caucvgprprlem1  7972  addcmpblnr  8002  mulcmpblnrlemg  8003  addsrmo  8006  mulsrmo  8007  addsrpr  8008  mulsrpr  8009  ltsrprg  8010  recexgt0sr  8036  mulgt0sr  8041  caucvgsrlemgt1  8058  caucvgsrlemoffval  8059  caucvgsr  8065  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  suplocsr  8072  mulcnsr  8098  pitoregt0  8112  recidpirqlemcalc  8120  axmulcom  8134  axmulass  8136  axdistr  8137  ax0id  8141  axcnre  8144  recriota  8153  axcaucvglemcau  8161  axcaucvglemres  8162  mulrid  8219  adddirp1d  8248  mul32  8351  mul31  8352  add32  8380  add4  8382  add42  8383  cnegex  8399  addcan2  8402  addsubass  8431  subsub2  8449  nppcan2  8452  sub32  8455  nnncan  8456  sub4  8466  muladd  8605  subdi  8606  mul2neg  8619  submul2  8620  mulsub  8622  muls1d  8639  mulsubfacd  8640  add20  8696  recexre  8800  rereim  8808  apreap  8809  ltmul1  8814  cru  8824  apreim  8825  mulreim  8826  apadd1  8830  apneg  8833  mulap0  8876  divrecap  8910  divassap  8912  divmulasscomap  8918  divsubdirap  8930  divdivdivap  8935  divmul24ap  8938  divmuleqap  8939  divcanap6  8941  divdivap1  8945  divdivap2  8946  divsubdivap  8950  conjmulap  8951  div2negap  8957  apmul1  9010  cju  9183  nnmulcl  9206  add1p1  9436  sub1m1  9437  cnm2m1cnm3  9438  xp1d2m1eqxm1d2  9439  div4p1lem1div2  9440  un0addcl  9477  un0mulcl  9478  zaddcllemneg  9562  qapne  9917  cnref1o  9929  rexsub  10132  xnegid  10138  xaddcom  10140  xnegdi  10147  xaddass  10148  xaddass2  10149  xpncan  10150  xnpcan  10151  xleadd1a  10152  xsubge0  10160  xposdif  10161  xlesubadd  10162  xadd4d  10164  lincmb01cmp  10282  iccf1o  10284  ige3m2fz  10329  fztp  10358  fzsuc2  10359  fseq1m1p1  10375  fzm1  10380  ige2m1fz1  10389  nn0split  10416  nnsplit  10417  fzo0addelr  10480  elfzoext  10483  fzval3  10495  zpnn0elfzo1  10499  fzosplitsnm1  10500  fzosplitpr  10525  fzosplitprm1  10526  fzoshftral  10530  rebtwn2zlemstep  10558  flhalf  10608  fldiv4lem1div2uz2  10612  modqval  10632  modqvalr  10633  modqdiffl  10643  modqfrac  10645  flqmod  10646  intqfrac  10647  zmod10  10648  modqmulnn  10650  modqvalp1  10651  modqid  10657  modqcyc  10667  modqcyc2  10668  modqmul1  10685  q2submod  10693  modqdi  10700  modqsubdir  10701  modqeqmodmin  10702  modsumfzodifsn  10704  addmodlteq  10706  frecuzrdgsuctlem  10731  uzsinds  10752  seqeq3  10760  iseqvalcbv  10767  seq3val  10768  seqvalcd  10769  seqf  10772  seq3p1  10773  seqovcd  10775  seqp1cd  10778  seq3m1  10781  seq3fveq2  10783  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  monoord2  10794  ser3mono  10795  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seqcaopr3g  10800  seq3caopr2  10801  seqcaopr2g  10802  seq3caopr  10803  seqcaoprg  10804  seqf1oglem2a  10826  seqf1oglem2  10828  seq3id2  10834  seq3homo  10835  seq3z  10836  seqhomog  10838  exp3vallem  10848  exp3val  10849  expp1  10854  expnegap0  10855  expineg2  10856  expn1ap0  10857  expm1t  10875  1exp  10876  expnegzap  10881  mulexpzap  10887  expadd  10889  expaddzaplem  10890  expaddzap  10891  expmul  10892  expmulzap  10893  m1expeven  10894  expsubap  10895  expp1zap  10896  expm1ap  10897  expdivap  10898  iexpcyc  10952  subsq2  10955  binom2  10959  binom21  10960  binom2sub  10961  binom2sub1  10962  mulbinom2  10964  binom3  10965  zesq  10966  bernneq  10968  sqoddm1div8  11001  mulsubdivbinom2ap  11019  nn0opthlem1d  11028  nn0opthd  11030  facp1  11038  facnn2  11042  faclbnd  11049  faclbnd6  11052  bcval  11057  bccmpl  11062  bcn0  11063  bcnn  11065  bcnp1n  11067  bcm1k  11068  bcp1n  11069  bcp1nk  11070  bcval5  11071  bcp1m1  11073  bcpasc  11074  bcn2m1  11077  bcn2p1  11078  omgadd  11111  hashunlem  11113  hashunsng  11117  hashdifsn  11129  hashxp  11136  zfz1isolemsplit  11148  zfz1isolem1  11150  zfz1iso  11151  seq3coll  11152  wrdf  11168  ccatfvalfi  11218  elfzelfzccat  11226  ccatlid  11232  ccatrid  11233  ccatass  11234  ccatalpha  11239  ccatws1leng  11260  ccats1val2  11266  ccatw2s1p1g  11271  swrdval  11278  swrd00g  11279  swrdf  11285  swrdfv2  11293  swrdwrdsymbg  11294  swrdspsleq  11297  swrds1  11298  swrdlsw  11299  ccatswrd  11300  swrdccat2  11301  pfxmpt  11310  pfxfv  11314  pfxeq  11326  pfxsuff1eqwrdeq  11329  ccatpfx  11331  pfxccat1  11332  swrdswrd  11335  pfxswrd  11336  swrdpfx  11337  pfxpfx  11338  pfxlswccat  11343  ccats1pfxeq  11344  ccats1pfxeqrex  11345  ccatopth2  11347  cats1un  11351  wrdind  11352  wrd2ind  11353  swrdccatfn  11354  swrdccatin1  11355  pfxccatin12lem4  11356  swrdccatin2  11359  pfxccatin12lem2c  11360  pfxccatin12lem2  11361  pfxccatin12  11363  swrdccat  11365  swrdccat3blem  11369  swrdccat3b  11370  swrdccatin2d  11374  pfxccatin12d  11375  reuccatpfxs1lem  11376  reuccatpfxs1  11377  shftcan1  11457  shftcan2  11458  cjval  11468  cjth  11469  crre  11480  replim  11482  remim  11483  reim0b  11485  rereb  11486  mulreap  11487  cjreb  11489  recj  11490  reneg  11491  readd  11492  resub  11493  remullem  11494  imcj  11498  imneg  11499  imadd  11500  imsub  11501  cjcj  11506  cjadd  11507  ipcnval  11509  cjmulrcl  11510  cjneg  11513  addcj  11514  cjsub  11515  cnrecnv  11533  caucvgrelemcau  11603  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniqlem  11617  resqrexlemover  11633  resqrexlemlo  11636  resqrexlemcalc1  11637  resqrexlemcalc3  11639  resqrexlemnm  11641  resqrexlemcvg  11642  absneg  11673  abscj  11675  sqabsadd  11678  sqabssub  11679  absmul  11692  absid  11694  absre  11700  absresq  11701  absexpzap  11703  recvalap  11720  abstri  11727  abs2dif2  11730  recan  11732  cau3lem  11737  amgm2  11741  bdtrilem  11862  xrmaxadd  11884  xrbdtri  11899  climaddc1  11952  climsubc1  11955  climcvg1nlem  11972  serf0  11975  fzf1o  11999  summodclem3  12004  summodclem2a  12005  summodc  12007  fsumsplitsn  12034  fsumm1  12040  fsumsplitsnun  12043  fsump1  12044  isummulc2  12050  fsumrev  12067  fisum0diag2  12071  fsummulc2  12072  fsumsub  12076  fsumabs  12089  telfsumo  12090  fsumparts  12094  fsumrelem  12095  fsumiun  12101  binomlem  12107  binom  12108  binom1p  12109  binom11  12110  binom1dif  12111  bcxmas  12113  isumsplit  12115  isum1p  12116  divcnv  12121  arisum2  12123  trireciplem  12124  trirecip  12125  geolim  12135  georeclim  12137  geo2sum  12138  geo2lim  12140  geoisum1c  12144  0.999...  12145  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratz  12156  mertenslem2  12160  mertensabs  12161  clim2prod  12163  prodfrecap  12170  prodfdivap  12171  prodmodclem3  12199  prodmodclem2a  12200  fprodm1  12222  fprodp1  12224  fprodunsn  12228  fprodfac  12239  fprodeq0  12241  fprodconst  12244  fprodrec  12253  fproddivap  12254  fprodsplitsn  12257  ege2le3  12295  efaddlem  12298  efsub  12305  efexp  12306  eftlub  12314  efsep  12315  effsumlt  12316  ef4p  12318  tanval3ap  12338  resinval  12339  recosval  12340  efi4p  12341  efival  12356  efmival  12357  efeul  12358  sinadd  12360  cosadd  12361  tanaddap  12363  sinsub  12364  cossub  12365  sincossq  12372  sin2t  12373  cos2t  12374  cos2tsin  12375  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  cos12dec  12392  absef  12394  absefib  12395  efieq1re  12396  demoivreALT  12398  eirraplem  12401  dvdsexp  12485  oexpneg  12501  opeo  12521  omeo  12522  m1exp1  12525  flodddiv4  12560  flodddiv4t2lthalf  12563  bitsval  12567  bitsp1  12575  bitsinv1lem  12585  bitsinv1  12586  divgcdnnr  12610  gcdaddm  12618  gcdadd  12619  gcdid  12620  modgcd  12625  gcdmultipled  12627  dvdsgcdidd  12628  bezoutlemnewy  12630  bezoutlema  12633  bezoutlemb  12634  bezoutlemex  12635  bezoutlembz  12638  absmulgcd  12651  gcdmultiple  12654  gcdmultiplez  12655  rpmulgcd  12660  rplpwr  12661  eucalginv  12691  eucalg  12694  lcmneg  12709  lcmgcdlem  12712  lcmgcd  12713  lcmid  12715  lcm1  12716  mulgcddvds  12729  qredeq  12731  divgcdcoprmex  12737  prmind2  12755  rpexp1i  12789  pw2dvdslemn  12800  pw2dvdseulemle  12802  pw2dvdseu  12803  oddpwdclemxy  12804  oddpwdclemdvds  12805  oddpwdclemndvds  12806  oddpwdclemdc  12808  2sqpwodd  12811  nn0gcdsq  12835  phiprmpw  12857  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  fermltl  12869  prmdiv  12870  hashgcdlem  12873  odzdvds  12881  vfermltl  12887  modprm0  12890  nnnn0modprm0  12891  modprmn0modprm0  12892  coprimeprodsq  12893  pythagtriplem1  12901  pythagtriplem4  12904  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  pythagtriplem18  12917  pythagtrip  12919  pcpremul  12929  pceu  12931  pczpre  12933  pcdiv  12938  pcqmul  12939  pcqdiv  12943  pcexp  12945  pcxqcl  12948  pczdvds  12950  pczndvds  12952  pczndvds2  12954  pcid  12960  pcneg  12961  pcdvdstr  12963  pcgcd1  12964  pcgcd  12965  pc2dvds  12966  pcaddlem  12975  pcadd  12976  pcadd2  12977  pcmpt  12979  pcmpt2  12980  fldivp1  12984  pcfac  12986  pcbc  12987  expnprm  12989  prmpwdvds  12991  pockthlem  12992  pockthi  12994  4sqlem7  13020  4sqlem9  13022  4sqlem10  13023  4sqlem2  13025  4sqlem3  13026  4sqlem4  13028  mul4sqlem  13029  4sqlem11  13037  4sqlem16  13042  4sqlem17  13043  4sqlem19  13045  setscomd  13186  ressvalsets  13210  strressid  13217  ressval3d  13218  ressinbasd  13220  ressressg  13221  ressabsg  13222  grpinvalem  13531  grpinva  13532  grprida  13533  isnsgrp  13552  sgrpass  13554  sgrp1  13557  sgrppropd  13559  prdssgrpd  13561  mnd32g  13573  mnd4g  13575  mndpropd  13586  prdsidlem  13593  prdsmndd  13594  imasmnd2  13598  mhmex  13608  mhmlin  13613  gsumwmhm  13644  grprcan  13683  grpsubval  13692  grpinvid2  13699  grpasscan2  13710  grpsubinv  13719  grpinvadd  13724  grpsubid1  13731  grpsubadd0sub  13733  grpsubadd  13734  grpsubsub  13735  grpaddsubass  13736  grppncan  13737  grpnnncan2  13743  grpsubpropd2  13751  imasgrp2  13760  mhmlem  13764  mhmid  13765  mhmmnd  13766  ghmgrp  13768  mulgnn0gsum  13778  mulgnnp1  13780  mulgaddcomlem  13795  mulgaddcom  13796  mulginvinv  13798  mulgnn0dir  13802  mulgdirlem  13803  mulgp1  13805  mulgneg2  13806  mulgnn0ass  13808  mulgass  13809  mulgmodid  13811  mulgsubdir  13812  nmzsubg  13860  0nsg  13864  eqger  13874  qussub  13887  ghmlin  13898  ghmsub  13901  conjghm  13926  ablsub4  13963  abladdsub4  13964  ablsubsub4  13969  ablsub32  13972  ablnnncan  13973  gsumfzmptfidmadd2  13990  gsumfzconst  13991  gsumfzmhm2  13994  gsumfzsnfd  13995  gsumsplit0  13996  mgpress  14008  rngass  14016  rngdi  14017  rngdir  14018  rngrz  14023  rngmneg2  14025  rngsubdi  14028  rngsubdir  14029  rngpropd  14032  imasrng  14033  srgass  14048  srgpcomp  14067  srgpcompp  14068  srgpcomppsc  14069  srg1expzeq1  14072  ringpropd  14115  ringrz  14121  ringnegr  14129  ringmneg2  14131  ringsubdi  14133  ringsubdir  14134  ring1  14136  imasring  14141  opprrng  14154  opprring  14156  mulgass3  14162  dvdsrd  14172  unitgrp  14194  invrfvald  14200  dvr1  14216  dvrass  14217  dvrcan1  14218  dvrcan3  14219  rdivmuldivd  14222  subrginv  14315  subrgdv  14316  resrhm2b  14327  rrgsupp  14344  islmod  14370  lmodlema  14371  islmodd  14372  lmodvs0  14401  lmodvneg1  14409  lmodvsubval2  14421  lmodsubvs  14422  lmodsubdi  14423  lmodsubdir  14424  lmodprop2d  14427  rmodislmodlem  14429  rmodislmod  14430  lsssn0  14449  sraval  14516  cnfldsub  14654  gsumfzfsumlem0  14665  gsumfzfsumlemm  14666  mulgrhm  14688  mulgrhm2  14689  znval  14715  znval2  14717  znunit  14738  psrval  14745  mplvalcoe  14774  mplval2g  14779  restabs  14969  cnprcl2k  15000  cnrest2r  15031  ispsmet  15117  psmettri2  15122  psmetsym  15123  ismet  15138  isxmet  15139  xmettri2  15155  xmetsym  15162  xmettri3  15168  mettri3  15169  xblss2ps  15198  xblss2  15199  comet  15293  xmetxp  15301  xmetxpbl  15302  txmetcnp  15312  fsumcncntop  15361  cncfi  15372  divcncfap  15408  limccl  15453  ellimc3apf  15454  limccnpcntop  15469  limccnp2lem  15470  reldvg  15473  dvfvalap  15475  eldvap  15476  dvcj  15503  dvfre  15504  dvexp  15505  dvexp2  15506  dvrecap  15507  dvmptaddx  15513  dvmptmulx  15514  dvmptnegcn  15516  dvmptsubcn  15517  dvmptcjx  15518  dvmptfsum  15519  dveflem  15520  dvef  15521  plyconst  15539  plyaddlem1  15541  plymullem1  15542  plyadd  15545  plymul  15546  plycoeid3  15551  plycolemc  15552  plyco  15553  plycjlemc  15554  plycj  15555  plyrecj  15557  dvply1  15559  dvply2g  15560  sin0pilem1  15575  sin0pilem2  15576  efper  15601  sinperlem  15602  efimpi  15613  ptolemy  15618  tangtx  15632  abssinper  15640  cosq34lt1  15644  rpcxpef  15688  rpcxpp1  15700  rpcxpneg  15701  rpcxpsub  15702  rpmulcxp  15703  rpdivcxp  15705  cxpmul  15706  rpcxpmul2  15707  rpcxproot  15708  cxpcom  15732  rpabscxpbnd  15734  rplogbval  15739  rplogbreexp  15747  rplogbzexp  15748  rprelogbmulexp  15750  rprelogbdiv  15751  relogbexpap  15752  rplogbcxp  15757  rpcxplogb  15758  logbgcd1irr  15761  logbgcd1irraplemap  15763  binom4  15773  pellexlem2  15775  pellexlem3  15776  wilthlem1  15777  sgmval  15780  sgmppw  15789  1sgmprm  15791  mersenne  15794  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgslem1  15802  lgsval  15806  lgsfvalg  15807  lgsval2lem  15812  lgsval4  15822  lgsneg  15826  lgsneg1  15827  lgsmod  15828  lgsdir2  15835  lgsdirprm  15836  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  lgssq2  15843  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  gausslemma2dlem2  15864  gausslemma2dlem3  15865  gausslemma2dlem4  15866  gausslemma2dlem5  15868  gausslemma2dlem6  15869  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem1  15883  lgsquad2lem2  15884  lgsquad2  15885  lgsquad3  15886  m1lgs  15887  2lgslem3c  15897  2lgslem3d  15898  2lgslem3d1  15902  2sqlem2  15917  2sqlem3  15919  2sqlem4  15920  2sqlem8  15925  2sqlem9  15926  2sqlem10  15927  vtxdumgrfival  16222  p1evtxdeqfi  16236  p1evtxdp1fi  16237  iswlk  16247  upgr2wlkdc  16301  wlkres  16303  trlreslem  16313  isclwwlk  16318  clwwlkccatlem  16324  clwwlknp  16341  clwwlkn1  16342  clwwlkn2  16345  clwwlkext2edg  16346  clwwlknonex2lem1  16361  clwwlknonex2lem2  16362  clwwlknonex2  16363  iseupth  16371  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  depindlem1  16430  qdencn  16738  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  trilpo  16758  apdifflemf  16761  apdiff  16763  iswomni0  16767  redcwlpolemeq1  16770  redcwlpo  16771  nconstwlpolem0  16779  nconstwlpolemgt0  16780  nconstwlpo  16782  neapmkv  16784  gfsumval  16792  gsumgfsum1  16793  gsumgfsum  16796  gfsumsn  16797  gfsump1  16798  gfsumcl  16799