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  10434  elfzoext  10437  fzval3  10449  zpnn0elfzo1  10453  fzosplitsnm1  10454  fzosplitpr  10479  fzosplitprm1  10480  fzoshftral  10484  rebtwn2zlemstep  10512  flhalf  10562  fldiv4lem1div2uz2  10566  modqval  10586  modqvalr  10587  modqdiffl  10597  modqfrac  10599  flqmod  10600  intqfrac  10601  zmod10  10602  modqmulnn  10604  modqvalp1  10605  modqid  10611  modqcyc  10621  modqcyc2  10622  modqmul1  10639  q2submod  10647  modqdi  10654  modqsubdir  10655  modqeqmodmin  10656  modsumfzodifsn  10658  addmodlteq  10660  frecuzrdgsuctlem  10685  uzsinds  10706  seqeq3  10714  iseqvalcbv  10721  seq3val  10722  seqvalcd  10723  seqf  10726  seq3p1  10727  seqovcd  10729  seqp1cd  10732  seq3m1  10735  seq3fveq2  10737  seqfveq2g  10739  seq3shft2  10743  seqshft2g  10744  monoord2  10748  ser3mono  10749  seq3split  10750  seqsplitg  10751  seq3caopr3  10753  seqcaopr3g  10754  seq3caopr2  10755  seqcaopr2g  10756  seq3caopr  10757  seqcaoprg  10758  seqf1oglem2a  10780  seqf1oglem2  10782  seq3id2  10788  seq3homo  10789  seq3z  10790  seqhomog  10792  exp3vallem  10802  exp3val  10803  expp1  10808  expnegap0  10809  expineg2  10810  expn1ap0  10811  expm1t  10829  1exp  10830  expnegzap  10835  mulexpzap  10841  expadd  10843  expaddzaplem  10844  expaddzap  10845  expmul  10846  expmulzap  10847  m1expeven  10848  expsubap  10849  expp1zap  10850  expm1ap  10851  expdivap  10852  iexpcyc  10906  subsq2  10909  binom2  10913  binom21  10914  binom2sub  10915  binom2sub1  10916  mulbinom2  10918  binom3  10919  zesq  10920  bernneq  10922  sqoddm1div8  10955  mulsubdivbinom2ap  10973  nn0opthlem1d  10982  nn0opthd  10984  facp1  10992  facnn2  10996  faclbnd  11003  faclbnd6  11006  bcval  11011  bccmpl  11016  bcn0  11017  bcnn  11019  bcnp1n  11021  bcm1k  11022  bcp1n  11023  bcp1nk  11024  bcval5  11025  bcp1m1  11027  bcpasc  11028  bcn2m1  11031  bcn2p1  11032  omgadd  11065  hashunlem  11067  hashunsng  11071  hashdifsn  11083  hashxp  11090  zfz1isolemsplit  11102  zfz1isolem1  11104  zfz1iso  11105  seq3coll  11106  wrdf  11119  ccatfvalfi  11169  elfzelfzccat  11177  ccatlid  11183  ccatrid  11184  ccatass  11185  ccatalpha  11190  ccatws1leng  11211  ccats1val2  11217  ccatw2s1p1g  11222  swrdval  11229  swrd00g  11230  swrdf  11236  swrdfv2  11244  swrdwrdsymbg  11245  swrdspsleq  11248  swrds1  11249  swrdlsw  11250  ccatswrd  11251  swrdccat2  11252  pfxmpt  11261  pfxfv  11265  pfxeq  11277  pfxsuff1eqwrdeq  11280  ccatpfx  11282  pfxccat1  11283  swrdswrd  11286  pfxswrd  11287  swrdpfx  11288  pfxpfx  11289  pfxlswccat  11294  ccats1pfxeq  11295  ccats1pfxeqrex  11296  ccatopth2  11298  cats1un  11302  wrdind  11303  wrd2ind  11304  swrdccatfn  11305  swrdccatin1  11306  pfxccatin12lem4  11307  swrdccatin2  11310  pfxccatin12lem2c  11311  pfxccatin12lem2  11312  pfxccatin12  11314  swrdccat  11316  swrdccat3blem  11320  swrdccat3b  11321  swrdccatin2d  11325  pfxccatin12d  11326  reuccatpfxs1lem  11327  reuccatpfxs1  11328  shftcan1  11395  shftcan2  11396  cjval  11406  cjth  11407  crre  11418  replim  11420  remim  11421  reim0b  11423  rereb  11424  mulreap  11425  cjreb  11427  recj  11428  reneg  11429  readd  11430  resub  11431  remullem  11432  imcj  11436  imneg  11437  imadd  11438  imsub  11439  cjcj  11444  cjadd  11445  ipcnval  11447  cjmulrcl  11448  cjneg  11451  addcj  11452  cjsub  11453  cnrecnv  11471  caucvgrelemcau  11541  cvg1nlemcau  11545  cvg1nlemres  11546  recvguniqlem  11555  resqrexlemover  11571  resqrexlemlo  11574  resqrexlemcalc1  11575  resqrexlemcalc3  11577  resqrexlemnm  11579  resqrexlemcvg  11580  absneg  11611  abscj  11613  sqabsadd  11616  sqabssub  11617  absmul  11630  absid  11632  absre  11638  absresq  11639  absexpzap  11641  recvalap  11658  abstri  11665  abs2dif2  11668  recan  11670  cau3lem  11675  amgm2  11679  bdtrilem  11800  xrmaxadd  11822  xrbdtri  11837  climaddc1  11890  climsubc1  11893  climcvg1nlem  11910  serf0  11913  fzf1o  11937  summodclem3  11942  summodclem2a  11943  summodc  11945  fsumsplitsn  11972  fsumm1  11978  fsumsplitsnun  11981  fsump1  11982  isummulc2  11988  fsumrev  12005  fisum0diag2  12009  fsummulc2  12010  fsumsub  12014  fsumabs  12027  telfsumo  12028  fsumparts  12032  fsumrelem  12033  fsumiun  12039  binomlem  12045  binom  12046  binom1p  12047  binom11  12048  binom1dif  12049  bcxmas  12051  isumsplit  12053  isum1p  12054  divcnv  12059  arisum2  12061  trireciplem  12062  trirecip  12063  geolim  12073  georeclim  12075  geo2sum  12076  geo2lim  12078  geoisum1c  12082  0.999...  12083  cvgratnnlemnexp  12086  cvgratnnlemmn  12087  cvgratz  12094  mertenslem2  12098  mertensabs  12099  clim2prod  12101  prodfrecap  12108  prodfdivap  12109  prodmodclem3  12137  prodmodclem2a  12138  fprodm1  12160  fprodp1  12162  fprodunsn  12166  fprodfac  12177  fprodeq0  12179  fprodconst  12182  fprodrec  12191  fproddivap  12192  fprodsplitsn  12195  ege2le3  12233  efaddlem  12236  efsub  12243  efexp  12244  eftlub  12252  efsep  12253  effsumlt  12254  ef4p  12256  tanval3ap  12276  resinval  12277  recosval  12278  efi4p  12279  efival  12294  efmival  12295  efeul  12296  sinadd  12298  cosadd  12299  tanaddap  12301  sinsub  12302  cossub  12303  sincossq  12310  sin2t  12311  cos2t  12312  cos2tsin  12313  ef01bndlem  12318  sin01bnd  12319  cos01bnd  12320  cos12dec  12330  absef  12332  absefib  12333  efieq1re  12334  demoivreALT  12336  eirraplem  12339  dvdsexp  12423  oexpneg  12439  opeo  12459  omeo  12460  m1exp1  12463  flodddiv4  12498  flodddiv4t2lthalf  12501  bitsval  12505  bitsp1  12513  bitsinv1lem  12523  bitsinv1  12524  divgcdnnr  12548  gcdaddm  12556  gcdadd  12557  gcdid  12558  modgcd  12563  gcdmultipled  12565  dvdsgcdidd  12566  bezoutlemnewy  12568  bezoutlema  12571  bezoutlemb  12572  bezoutlemex  12573  bezoutlembz  12576  absmulgcd  12589  gcdmultiple  12592  gcdmultiplez  12593  rpmulgcd  12598  rplpwr  12599  eucalginv  12629  eucalg  12632  lcmneg  12647  lcmgcdlem  12650  lcmgcd  12651  lcmid  12653  lcm1  12654  mulgcddvds  12667  qredeq  12669  divgcdcoprmex  12675  prmind2  12693  rpexp1i  12727  pw2dvdslemn  12738  pw2dvdseulemle  12740  pw2dvdseu  12741  oddpwdclemxy  12742  oddpwdclemdvds  12743  oddpwdclemndvds  12744  oddpwdclemdc  12746  2sqpwodd  12749  nn0gcdsq  12773  phiprmpw  12795  eulerthlemrprm  12802  eulerthlema  12803  eulerthlemh  12804  eulerthlemth  12805  fermltl  12807  prmdiv  12808  hashgcdlem  12811  odzdvds  12819  vfermltl  12825  modprm0  12828  nnnn0modprm0  12829  modprmn0modprm0  12830  coprimeprodsq  12831  pythagtriplem1  12839  pythagtriplem4  12842  pythagtriplem12  12849  pythagtriplem14  12851  pythagtriplem16  12853  pythagtriplem18  12855  pythagtrip  12857  pcpremul  12867  pceu  12869  pczpre  12871  pcdiv  12876  pcqmul  12877  pcqdiv  12881  pcexp  12883  pcxqcl  12886  pczdvds  12888  pczndvds  12890  pczndvds2  12892  pcid  12898  pcneg  12899  pcdvdstr  12901  pcgcd1  12902  pcgcd  12903  pc2dvds  12904  pcaddlem  12913  pcadd  12914  pcadd2  12915  pcmpt  12917  pcmpt2  12918  fldivp1  12922  pcfac  12924  pcbc  12925  expnprm  12927  prmpwdvds  12929  pockthlem  12930  pockthi  12932  4sqlem7  12958  4sqlem9  12960  4sqlem10  12961  4sqlem2  12963  4sqlem3  12964  4sqlem4  12966  mul4sqlem  12967  4sqlem11  12975  4sqlem16  12980  4sqlem17  12981  4sqlem19  12983  setscomd  13124  ressvalsets  13148  strressid  13155  ressval3d  13156  ressinbasd  13158  ressressg  13159  ressabsg  13160  grpinvalem  13469  grpinva  13470  grprida  13471  isnsgrp  13490  sgrpass  13492  sgrp1  13495  sgrppropd  13497  prdssgrpd  13499  mnd32g  13511  mnd4g  13513  mndpropd  13524  prdsidlem  13531  prdsmndd  13532  imasmnd2  13536  mhmex  13546  mhmlin  13551  gsumwmhm  13582  grprcan  13621  grpsubval  13630  grpinvid2  13637  grpasscan2  13648  grpsubinv  13657  grpinvadd  13662  grpsubid1  13669  grpsubadd0sub  13671  grpsubadd  13672  grpsubsub  13673  grpaddsubass  13674  grppncan  13675  grpnnncan2  13681  grpsubpropd2  13689  imasgrp2  13698  mhmlem  13702  mhmid  13703  mhmmnd  13704  ghmgrp  13706  mulgnn0gsum  13716  mulgnnp1  13718  mulgaddcomlem  13733  mulgaddcom  13734  mulginvinv  13736  mulgnn0dir  13740  mulgdirlem  13741  mulgp1  13743  mulgneg2  13744  mulgnn0ass  13746  mulgass  13747  mulgmodid  13749  mulgsubdir  13750  nmzsubg  13798  0nsg  13802  eqger  13812  qussub  13825  ghmlin  13836  ghmsub  13839  conjghm  13864  ablsub4  13901  abladdsub4  13902  ablsubsub4  13907  ablsub32  13910  ablnnncan  13911  gsumfzmptfidmadd2  13928  gsumfzconst  13929  gsumfzmhm2  13932  gsumfzsnfd  13933  gsumsplit0  13934  mgpress  13946  rngass  13954  rngdi  13955  rngdir  13956  rngrz  13961  rngmneg2  13963  rngsubdi  13966  rngsubdir  13967  rngpropd  13970  imasrng  13971  srgass  13986  srgpcomp  14005  srgpcompp  14006  srgpcomppsc  14007  srg1expzeq1  14010  ringpropd  14053  ringrz  14059  ringnegr  14067  ringmneg2  14069  ringsubdi  14071  ringsubdir  14072  ring1  14074  imasring  14079  opprrng  14092  opprring  14094  mulgass3  14100  dvdsrd  14110  unitgrp  14132  invrfvald  14138  dvr1  14154  dvrass  14155  dvrcan1  14156  dvrcan3  14157  rdivmuldivd  14160  subrginv  14253  subrgdv  14254  resrhm2b  14265  islmod  14307  lmodlema  14308  islmodd  14309  lmodvs0  14338  lmodvneg1  14346  lmodvsubval2  14358  lmodsubvs  14359  lmodsubdi  14360  lmodsubdir  14361  lmodprop2d  14364  rmodislmodlem  14366  rmodislmod  14367  lsssn0  14386  sraval  14453  cnfldsub  14591  gsumfzfsumlem0  14602  gsumfzfsumlemm  14603  mulgrhm  14625  mulgrhm2  14626  znval  14652  znval2  14654  znunit  14675  psrval  14682  mplvalcoe  14706  mplval2g  14711  restabs  14901  cnprcl2k  14932  cnrest2r  14963  ispsmet  15049  psmettri2  15054  psmetsym  15055  ismet  15070  isxmet  15071  xmettri2  15087  xmetsym  15094  xmettri3  15100  mettri3  15101  xblss2ps  15130  xblss2  15131  comet  15225  xmetxp  15233  xmetxpbl  15234  txmetcnp  15244  fsumcncntop  15293  cncfi  15304  divcncfap  15340  limccl  15385  ellimc3apf  15386  limccnpcntop  15401  limccnp2lem  15402  reldvg  15405  dvfvalap  15407  eldvap  15408  dvcj  15435  dvfre  15436  dvexp  15437  dvexp2  15438  dvrecap  15439  dvmptaddx  15445  dvmptmulx  15446  dvmptnegcn  15448  dvmptsubcn  15449  dvmptcjx  15450  dvmptfsum  15451  dveflem  15452  dvef  15453  plyconst  15471  plyaddlem1  15473  plymullem1  15474  plyadd  15477  plymul  15478  plycoeid3  15483  plycolemc  15484  plyco  15485  plycjlemc  15486  plycj  15487  plyrecj  15489  dvply1  15491  dvply2g  15492  sin0pilem1  15507  sin0pilem2  15508  efper  15533  sinperlem  15534  efimpi  15545  ptolemy  15550  tangtx  15564  abssinper  15572  cosq34lt1  15576  rpcxpef  15620  rpcxpp1  15632  rpcxpneg  15633  rpcxpsub  15634  rpmulcxp  15635  rpdivcxp  15637  cxpmul  15638  rpcxpmul2  15639  rpcxproot  15640  cxpcom  15664  rpabscxpbnd  15666  rplogbval  15671  rplogbreexp  15679  rplogbzexp  15680  rprelogbmulexp  15682  rprelogbdiv  15683  relogbexpap  15684  rplogbcxp  15689  rpcxplogb  15690  logbgcd1irr  15693  logbgcd1irraplemap  15695  binom4  15705  wilthlem1  15706  sgmval  15709  sgmppw  15718  1sgmprm  15720  mersenne  15723  perfectlem1  15725  perfectlem2  15726  perfect  15727  lgslem1  15731  lgsval  15735  lgsfvalg  15736  lgsval2lem  15741  lgsval4  15751  lgsneg  15755  lgsneg1  15756  lgsmod  15757  lgsdir2  15764  lgsdirprm  15765  lgsdilem2  15767  lgsdi  15768  lgsne0  15769  lgssq2  15772  lgsdirnn0  15778  lgsdinn0  15779  gausslemma2dlem1a  15789  gausslemma2dlem1f1o  15791  gausslemma2dlem2  15793  gausslemma2dlem3  15794  gausslemma2dlem4  15795  gausslemma2dlem5  15797  gausslemma2dlem6  15798  gausslemma2d  15800  lgseisenlem1  15801  lgseisenlem2  15802  lgseisenlem3  15803  lgseisenlem4  15804  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  lgsquad2lem1  15812  lgsquad2lem2  15813  lgsquad2  15814  lgsquad3  15815  m1lgs  15816  2lgslem3c  15826  2lgslem3d  15827  2lgslem3d1  15831  2sqlem2  15846  2sqlem3  15848  2sqlem4  15849  2sqlem8  15854  2sqlem9  15855  2sqlem10  15856  vtxdumgrfival  16151  p1evtxdeqfi  16165  p1evtxdp1fi  16166  iswlk  16176  upgr2wlkdc  16230  wlkres  16232  trlreslem  16242  isclwwlk  16247  clwwlkccatlem  16253  clwwlknp  16270  clwwlkn1  16271  clwwlkn2  16274  clwwlkext2edg  16275  clwwlknonex2lem1  16290  clwwlknonex2lem2  16291  clwwlknonex2  16292  iseupth  16300  qdencn  16634  trilpolemclim  16643  trilpolemcl  16644  trilpolemisumle  16645  trilpolemeq1  16647  trilpolemlt1  16648  trilpo  16650  apdifflemf  16653  apdiff  16655  iswomni0  16658  redcwlpolemeq1  16661  redcwlpo  16662  nconstwlpolem0  16670  nconstwlpolemgt0  16671  nconstwlpo  16673  neapmkv  16675  gfsumval  16683  gsumgfsum1  16684  gsumgfsum  16687  gfsumsn  16688  gfsump1  16689  gfsumcl  16690