Theorem oveq2d 6029

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

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6013

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  csbov1g  6054  caovassg  6176  caovdig  6192  caovdirg  6195  caov32d  6198  caov4d  6202  caov42d  6204  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  addasspig  7540  mulasspig  7542  distrpig  7543  dfplpq2  7564  mulpipq2  7581  addassnqg  7592  prarloclemarch  7628  prarloclemarch2  7629  ltrnqg  7630  enq0sym  7642  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  nq0a0  7667  distrnq0  7669  addassnq0  7672  prarloclemlo  7704  prarloclem3  7707  prarloclem5  7710  prarloclemcalc  7712  addnqprl  7739  addnqpru  7740  prmuloclemcalc  7775  mulnqprl  7778  mulnqpru  7779  distrlem4prl  7794  distrlem4pru  7795  1idprl  7800  1idpru  7801  ltexprlemloc  7817  addcanprleml  7824  addcanprlemu  7825  recexprlem1ssu  7844  ltmprr  7852  caucvgprlemcanl  7854  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlemlim  7871  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkeqj  7900  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexb  7917  caucvgprprlemaddq  7918  caucvgprprlem1  7919  addcmpblnr  7949  mulcmpblnrlemg  7950  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  ltsrprg  7957  recexgt0sr  7983  mulgt0sr  7988  caucvgsrlemgt1  8005  caucvgsrlemoffval  8006  caucvgsr  8012  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  suplocsr  8019  mulcnsr  8045  pitoregt0  8059  recidpirqlemcalc  8067  axmulcom  8081  axmulass  8083  axdistr  8084  ax0id  8088  axcnre  8091  recriota  8100  axcaucvglemcau  8108  axcaucvglemres  8109  mulrid  8166  adddirp1d  8196  mul32  8299  mul31  8300  add32  8328  add4  8330  add42  8331  cnegex  8347  addcan2  8350  addsubass  8379  subsub2  8397  nppcan2  8400  sub32  8403  nnncan  8404  sub4  8414  muladd  8553  subdi  8554  mul2neg  8567  submul2  8568  mulsub  8570  muls1d  8587  mulsubfacd  8588  add20  8644  recexre  8748  rereim  8756  apreap  8757  ltmul1  8762  cru  8772  apreim  8773  mulreim  8774  apadd1  8778  apneg  8781  mulap0  8824  divrecap  8858  divassap  8860  divmulasscomap  8866  divsubdirap  8878  divdivdivap  8883  divmul24ap  8886  divmuleqap  8887  divcanap6  8889  divdivap1  8893  divdivap2  8894  divsubdivap  8898  conjmulap  8899  div2negap  8905  apmul1  8958  cju  9131  nnmulcl  9154  add1p1  9384  sub1m1  9385  cnm2m1cnm3  9386  xp1d2m1eqxm1d2  9387  div4p1lem1div2  9388  un0addcl  9425  un0mulcl  9426  zaddcllemneg  9508  qapne  9863  cnref1o  9875  rexsub  10078  xnegid  10084  xaddcom  10086  xnegdi  10093  xaddass  10094  xaddass2  10095  xpncan  10096  xnpcan  10097  xleadd1a  10098  xsubge0  10106  xposdif  10107  xlesubadd  10108  xadd4d  10110  lincmb01cmp  10228  iccf1o  10229  ige3m2fz  10274  fztp  10303  fzsuc2  10304  fseq1m1p1  10320  fzm1  10325  ige2m1fz1  10334  nn0split  10361  nnsplit  10362  fzo0addelr  10424  elfzoext  10427  fzval3  10439  zpnn0elfzo1  10443  fzosplitsnm1  10444  fzosplitpr  10469  fzosplitprm1  10470  fzoshftral  10474  rebtwn2zlemstep  10502  flhalf  10552  fldiv4lem1div2uz2  10556  modqval  10576  modqvalr  10577  modqdiffl  10587  modqfrac  10589  flqmod  10590  intqfrac  10591  zmod10  10592  modqmulnn  10594  modqvalp1  10595  modqid  10601  modqcyc  10611  modqcyc2  10612  modqmul1  10629  q2submod  10637  modqdi  10644  modqsubdir  10645  modqeqmodmin  10646  modsumfzodifsn  10648  addmodlteq  10650  frecuzrdgsuctlem  10675  uzsinds  10696  seqeq3  10704  iseqvalcbv  10711  seq3val  10712  seqvalcd  10713  seqf  10716  seq3p1  10717  seqovcd  10719  seqp1cd  10722  seq3m1  10725  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord2  10738  ser3mono  10739  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seq3caopr2  10745  seqcaopr2g  10746  seq3caopr  10747  seqcaoprg  10748  seqf1oglem2a  10770  seqf1oglem2  10772  seq3id2  10778  seq3homo  10779  seq3z  10780  seqhomog  10782  exp3vallem  10792  exp3val  10793  expp1  10798  expnegap0  10799  expineg2  10800  expn1ap0  10801  expm1t  10819  1exp  10820  expnegzap  10825  mulexpzap  10831  expadd  10833  expaddzaplem  10834  expaddzap  10835  expmul  10836  expmulzap  10837  m1expeven  10838  expsubap  10839  expp1zap  10840  expm1ap  10841  expdivap  10842  iexpcyc  10896  subsq2  10899  binom2  10903  binom21  10904  binom2sub  10905  binom2sub1  10906  mulbinom2  10908  binom3  10909  zesq  10910  bernneq  10912  sqoddm1div8  10945  mulsubdivbinom2ap  10963  nn0opthlem1d  10972  nn0opthd  10974  facp1  10982  facnn2  10986  faclbnd  10993  faclbnd6  10996  bcval  11001  bccmpl  11006  bcn0  11007  bcnn  11009  bcnp1n  11011  bcm1k  11012  bcp1n  11013  bcp1nk  11014  bcval5  11015  bcp1m1  11017  bcpasc  11018  bcn2m1  11021  bcn2p1  11022  omgadd  11055  hashunlem  11057  hashunsng  11061  hashdifsn  11073  hashxp  11080  zfz1isolemsplit  11092  zfz1isolem1  11094  zfz1iso  11095  seq3coll  11096  wrdf  11109  ccatfvalfi  11159  elfzelfzccat  11167  ccatlid  11173  ccatrid  11174  ccatass  11175  ccatalpha  11180  ccatws1leng  11201  ccats1val2  11207  ccatw2s1p1g  11212  swrdval  11219  swrd00g  11220  swrdf  11226  swrdfv2  11234  swrdwrdsymbg  11235  swrdspsleq  11238  swrds1  11239  swrdlsw  11240  ccatswrd  11241  swrdccat2  11242  pfxmpt  11251  pfxfv  11255  pfxeq  11267  pfxsuff1eqwrdeq  11270  ccatpfx  11272  pfxccat1  11273  swrdswrd  11276  pfxswrd  11277  swrdpfx  11278  pfxpfx  11279  pfxlswccat  11284  ccats1pfxeq  11285  ccats1pfxeqrex  11286  ccatopth2  11288  cats1un  11292  wrdind  11293  wrd2ind  11294  swrdccatfn  11295  swrdccatin1  11296  pfxccatin12lem4  11297  swrdccatin2  11300  pfxccatin12lem2c  11301  pfxccatin12lem2  11302  pfxccatin12  11304  swrdccat  11306  swrdccat3blem  11310  swrdccat3b  11311  swrdccatin2d  11315  pfxccatin12d  11316  reuccatpfxs1lem  11317  reuccatpfxs1  11318  shftcan1  11385  shftcan2  11386  cjval  11396  cjth  11397  crre  11408  replim  11410  remim  11411  reim0b  11413  rereb  11414  mulreap  11415  cjreb  11417  recj  11418  reneg  11419  readd  11420  resub  11421  remullem  11422  imcj  11426  imneg  11427  imadd  11428  imsub  11429  cjcj  11434  cjadd  11435  ipcnval  11437  cjmulrcl  11438  cjneg  11441  addcj  11442  cjsub  11443  cnrecnv  11461  caucvgrelemcau  11531  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniqlem  11545  resqrexlemover  11561  resqrexlemlo  11564  resqrexlemcalc1  11565  resqrexlemcalc3  11567  resqrexlemnm  11569  resqrexlemcvg  11570  absneg  11601  abscj  11603  sqabsadd  11606  sqabssub  11607  absmul  11620  absid  11622  absre  11628  absresq  11629  absexpzap  11631  recvalap  11648  abstri  11655  abs2dif2  11658  recan  11660  cau3lem  11665  amgm2  11669  bdtrilem  11790  xrmaxadd  11812  xrbdtri  11827  climaddc1  11880  climsubc1  11883  climcvg1nlem  11900  serf0  11903  summodclem3  11931  summodclem2a  11932  summodc  11934  fsumsplitsn  11961  fsumm1  11967  fsumsplitsnun  11970  fsump1  11971  isummulc2  11977  fsumrev  11994  fisum0diag2  11998  fsummulc2  11999  fsumsub  12003  fsumabs  12016  telfsumo  12017  fsumparts  12021  fsumrelem  12022  fsumiun  12028  binomlem  12034  binom  12035  binom1p  12036  binom11  12037  binom1dif  12038  bcxmas  12040  isumsplit  12042  isum1p  12043  divcnv  12048  arisum2  12050  trireciplem  12051  trirecip  12052  geolim  12062  georeclim  12064  geo2sum  12065  geo2lim  12067  geoisum1c  12071  0.999...  12072  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratz  12083  mertenslem2  12087  mertensabs  12088  clim2prod  12090  prodfrecap  12097  prodfdivap  12098  prodmodclem3  12126  prodmodclem2a  12127  fprodm1  12149  fprodp1  12151  fprodunsn  12155  fprodfac  12166  fprodeq0  12168  fprodconst  12171  fprodrec  12180  fproddivap  12181  fprodsplitsn  12184  ege2le3  12222  efaddlem  12225  efsub  12232  efexp  12233  eftlub  12241  efsep  12242  effsumlt  12243  ef4p  12245  tanval3ap  12265  resinval  12266  recosval  12267  efi4p  12268  efival  12283  efmival  12284  efeul  12285  sinadd  12287  cosadd  12288  tanaddap  12290  sinsub  12291  cossub  12292  sincossq  12299  sin2t  12300  cos2t  12301  cos2tsin  12302  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos12dec  12319  absef  12321  absefib  12322  efieq1re  12323  demoivreALT  12325  eirraplem  12328  dvdsexp  12412  oexpneg  12428  opeo  12448  omeo  12449  m1exp1  12452  flodddiv4  12487  flodddiv4t2lthalf  12490  bitsval  12494  bitsp1  12502  bitsinv1lem  12512  bitsinv1  12513  divgcdnnr  12537  gcdaddm  12545  gcdadd  12546  gcdid  12547  modgcd  12552  gcdmultipled  12554  dvdsgcdidd  12555  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  bezoutlemex  12562  bezoutlembz  12565  absmulgcd  12578  gcdmultiple  12581  gcdmultiplez  12582  rpmulgcd  12587  rplpwr  12588  eucalginv  12618  eucalg  12621  lcmneg  12636  lcmgcdlem  12639  lcmgcd  12640  lcmid  12642  lcm1  12643  mulgcddvds  12656  qredeq  12658  divgcdcoprmex  12664  prmind2  12682  rpexp1i  12716  pw2dvdslemn  12727  pw2dvdseulemle  12729  pw2dvdseu  12730  oddpwdclemxy  12731  oddpwdclemdvds  12732  oddpwdclemndvds  12733  oddpwdclemdc  12735  2sqpwodd  12738  nn0gcdsq  12762  phiprmpw  12784  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  fermltl  12796  prmdiv  12797  hashgcdlem  12800  odzdvds  12808  vfermltl  12814  modprm0  12817  nnnn0modprm0  12818  modprmn0modprm0  12819  coprimeprodsq  12820  pythagtriplem1  12828  pythagtriplem4  12831  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  pythagtriplem18  12844  pythagtrip  12846  pcpremul  12856  pceu  12858  pczpre  12860  pcdiv  12865  pcqmul  12866  pcqdiv  12870  pcexp  12872  pcxqcl  12875  pczdvds  12877  pczndvds  12879  pczndvds2  12881  pcid  12887  pcneg  12888  pcdvdstr  12890  pcgcd1  12891  pcgcd  12892  pc2dvds  12893  pcaddlem  12902  pcadd  12903  pcadd2  12904  pcmpt  12906  pcmpt2  12907  fldivp1  12911  pcfac  12913  pcbc  12914  expnprm  12916  prmpwdvds  12918  pockthlem  12919  pockthi  12921  4sqlem7  12947  4sqlem9  12949  4sqlem10  12950  4sqlem2  12952  4sqlem3  12953  4sqlem4  12955  mul4sqlem  12956  4sqlem11  12964  4sqlem16  12969  4sqlem17  12970  4sqlem19  12972  setscomd  13113  ressvalsets  13137  strressid  13144  ressval3d  13145  ressinbasd  13147  ressressg  13148  ressabsg  13149  grpinvalem  13458  grpinva  13459  grprida  13460  isnsgrp  13479  sgrpass  13481  sgrp1  13484  sgrppropd  13486  prdssgrpd  13488  mnd32g  13500  mnd4g  13502  mndpropd  13513  prdsidlem  13520  prdsmndd  13521  imasmnd2  13525  mhmex  13535  mhmlin  13540  gsumwmhm  13571  grprcan  13610  grpsubval  13619  grpinvid2  13626  grpasscan2  13637  grpsubinv  13646  grpinvadd  13651  grpsubid1  13658  grpsubadd0sub  13660  grpsubadd  13661  grpsubsub  13662  grpaddsubass  13663  grppncan  13664  grpnnncan2  13670  grpsubpropd2  13678  imasgrp2  13687  mhmlem  13691  mhmid  13692  mhmmnd  13693  ghmgrp  13695  mulgnn0gsum  13705  mulgnnp1  13707  mulgaddcomlem  13722  mulgaddcom  13723  mulginvinv  13725  mulgnn0dir  13729  mulgdirlem  13730  mulgp1  13732  mulgneg2  13733  mulgnn0ass  13735  mulgass  13736  mulgmodid  13738  mulgsubdir  13739  nmzsubg  13787  0nsg  13791  eqger  13801  qussub  13814  ghmlin  13825  ghmsub  13828  conjghm  13853  ablsub4  13890  abladdsub4  13891  ablsubsub4  13896  ablsub32  13899  ablnnncan  13900  gsumfzmptfidmadd2  13917  gsumfzconst  13918  gsumfzmhm2  13921  gsumfzsnfd  13922  mgpress  13934  rngass  13942  rngdi  13943  rngdir  13944  rngrz  13949  rngmneg2  13951  rngsubdi  13954  rngsubdir  13955  rngpropd  13958  imasrng  13959  srgass  13974  srgpcomp  13993  srgpcompp  13994  srgpcomppsc  13995  srg1expzeq1  13998  ringpropd  14041  ringrz  14047  ringnegr  14055  ringmneg2  14057  ringsubdi  14059  ringsubdir  14060  ring1  14062  imasring  14067  opprrng  14080  opprring  14082  mulgass3  14088  dvdsrd  14098  unitgrp  14120  invrfvald  14126  dvr1  14142  dvrass  14143  dvrcan1  14144  dvrcan3  14145  rdivmuldivd  14148  subrginv  14241  subrgdv  14242  resrhm2b  14253  islmod  14295  lmodlema  14296  islmodd  14297  lmodvs0  14326  lmodvneg1  14334  lmodvsubval2  14346  lmodsubvs  14347  lmodsubdi  14348  lmodsubdir  14349  lmodprop2d  14352  rmodislmodlem  14354  rmodislmod  14355  lsssn0  14374  sraval  14441  cnfldsub  14579  gsumfzfsumlem0  14590  gsumfzfsumlemm  14591  mulgrhm  14613  mulgrhm2  14614  znval  14640  znval2  14642  znunit  14663  psrval  14670  mplvalcoe  14694  mplval2g  14699  restabs  14889  cnprcl2k  14920  cnrest2r  14951  ispsmet  15037  psmettri2  15042  psmetsym  15043  ismet  15058  isxmet  15059  xmettri2  15075  xmetsym  15082  xmettri3  15088  mettri3  15089  xblss2ps  15118  xblss2  15119  comet  15213  xmetxp  15221  xmetxpbl  15222  txmetcnp  15232  fsumcncntop  15281  cncfi  15292  divcncfap  15328  limccl  15373  ellimc3apf  15374  limccnpcntop  15389  limccnp2lem  15390  reldvg  15393  dvfvalap  15395  eldvap  15396  dvcj  15423  dvfre  15424  dvexp  15425  dvexp2  15426  dvrecap  15427  dvmptaddx  15433  dvmptmulx  15434  dvmptnegcn  15436  dvmptsubcn  15437  dvmptcjx  15438  dvmptfsum  15439  dveflem  15440  dvef  15441  plyconst  15459  plyaddlem1  15461  plymullem1  15462  plyadd  15465  plymul  15466  plycoeid3  15471  plycolemc  15472  plyco  15473  plycjlemc  15474  plycj  15475  plyrecj  15477  dvply1  15479  dvply2g  15480  sin0pilem1  15495  sin0pilem2  15496  efper  15521  sinperlem  15522  efimpi  15533  ptolemy  15538  tangtx  15552  abssinper  15560  cosq34lt1  15564  rpcxpef  15608  rpcxpp1  15620  rpcxpneg  15621  rpcxpsub  15622  rpmulcxp  15623  rpdivcxp  15625  cxpmul  15626  rpcxpmul2  15627  rpcxproot  15628  cxpcom  15652  rpabscxpbnd  15654  rplogbval  15659  rplogbreexp  15667  rplogbzexp  15668  rprelogbmulexp  15670  rprelogbdiv  15671  relogbexpap  15672  rplogbcxp  15677  rpcxplogb  15678  logbgcd1irr  15681  logbgcd1irraplemap  15683  binom4  15693  wilthlem1  15694  sgmval  15697  sgmppw  15706  1sgmprm  15708  mersenne  15711  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgslem1  15719  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsval4  15739  lgsneg  15743  lgsneg1  15744  lgsmod  15745  lgsdir2  15752  lgsdirprm  15753  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgssq2  15760  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem2  15781  gausslemma2dlem3  15782  gausslemma2dlem4  15783  gausslemma2dlem5  15785  gausslemma2dlem6  15786  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  lgsquad2lem2  15801  lgsquad2  15802  lgsquad3  15803  m1lgs  15804  2lgslem3c  15814  2lgslem3d  15815  2lgslem3d1  15819  2sqlem2  15834  2sqlem3  15836  2sqlem4  15837  2sqlem8  15842  2sqlem9  15843  2sqlem10  15844  vtxdumgrfival  16104  iswlk  16120  upgr2wlkdc  16172  wlkres  16174  trlreslem  16184  isclwwlk  16189  clwwlkccatlem  16195  clwwlknp  16212  clwwlkn1  16213  clwwlkn2  16216  clwwlkext2edg  16217  clwwlknonex2lem1  16232  clwwlknonex2lem2  16233  clwwlknonex2  16234  iseupth  16242  qdencn  16567  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trilpo  16583  apdifflemf  16586  apdiff  16588  iswomni0  16591  redcwlpolemeq1  16594  redcwlpo  16595  nconstwlpolem0  16603  nconstwlpolemgt0  16604  nconstwlpo  16606  neapmkv  16608