Theorem oveq2d 6033

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

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

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 6020

This theorem is referenced by:  csbov1g  6058  caovassg  6180  caovdig  6196  caovdirg  6199  caov32d  6202  caov4d  6206  caov42d  6208  nnaass  6652  nndi  6653  nnmass  6654  nnmsucr  6655  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  addasspig  7549  mulasspig  7551  distrpig  7552  dfplpq2  7573  mulpipq2  7590  addassnqg  7601  prarloclemarch  7637  prarloclemarch2  7638  ltrnqg  7639  enq0sym  7651  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  nq0a0  7676  distrnq0  7678  addassnq0  7681  prarloclemlo  7713  prarloclem3  7716  prarloclem5  7719  prarloclemcalc  7721  addnqprl  7748  addnqpru  7749  prmuloclemcalc  7784  mulnqprl  7787  mulnqpru  7788  distrlem4prl  7803  distrlem4pru  7804  1idprl  7809  1idpru  7810  ltexprlemloc  7826  addcanprleml  7833  addcanprlemu  7834  recexprlem1ssu  7853  ltmprr  7861  caucvgprlemcanl  7863  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlemlim  7880  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkeqj  7909  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexb  7926  caucvgprprlemaddq  7927  caucvgprprlem1  7928  addcmpblnr  7958  mulcmpblnrlemg  7959  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  ltsrprg  7966  recexgt0sr  7992  mulgt0sr  7997  caucvgsrlemgt1  8014  caucvgsrlemoffval  8015  caucvgsr  8021  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  suplocsr  8028  mulcnsr  8054  pitoregt0  8068  recidpirqlemcalc  8076  axmulcom  8090  axmulass  8092  axdistr  8093  ax0id  8097  axcnre  8100  recriota  8109  axcaucvglemcau  8117  axcaucvglemres  8118  mulrid  8175  adddirp1d  8205  mul32  8308  mul31  8309  add32  8337  add4  8339  add42  8340  cnegex  8356  addcan2  8359  addsubass  8388  subsub2  8406  nppcan2  8409  sub32  8412  nnncan  8413  sub4  8423  muladd  8562  subdi  8563  mul2neg  8576  submul2  8577  mulsub  8579  muls1d  8596  mulsubfacd  8597  add20  8653  recexre  8757  rereim  8765  apreap  8766  ltmul1  8771  cru  8781  apreim  8782  mulreim  8783  apadd1  8787  apneg  8790  mulap0  8833  divrecap  8867  divassap  8869  divmulasscomap  8875  divsubdirap  8887  divdivdivap  8892  divmul24ap  8895  divmuleqap  8896  divcanap6  8898  divdivap1  8902  divdivap2  8903  divsubdivap  8907  conjmulap  8908  div2negap  8914  apmul1  8967  cju  9140  nnmulcl  9163  add1p1  9393  sub1m1  9394  cnm2m1cnm3  9395  xp1d2m1eqxm1d2  9396  div4p1lem1div2  9397  un0addcl  9434  un0mulcl  9435  zaddcllemneg  9517  qapne  9872  cnref1o  9884  rexsub  10087  xnegid  10093  xaddcom  10095  xnegdi  10102  xaddass  10103  xaddass2  10104  xpncan  10105  xnpcan  10106  xleadd1a  10107  xsubge0  10115  xposdif  10116  xlesubadd  10117  xadd4d  10119  lincmb01cmp  10237  iccf1o  10238  ige3m2fz  10283  fztp  10312  fzsuc2  10313  fseq1m1p1  10329  fzm1  10334  ige2m1fz1  10343  nn0split  10370  nnsplit  10371  fzo0addelr  10433  elfzoext  10436  fzval3  10448  zpnn0elfzo1  10452  fzosplitsnm1  10453  fzosplitpr  10478  fzosplitprm1  10479  fzoshftral  10483  rebtwn2zlemstep  10511  flhalf  10561  fldiv4lem1div2uz2  10565  modqval  10585  modqvalr  10586  modqdiffl  10596  modqfrac  10598  flqmod  10599  intqfrac  10600  zmod10  10601  modqmulnn  10603  modqvalp1  10604  modqid  10610  modqcyc  10620  modqcyc2  10621  modqmul1  10638  q2submod  10646  modqdi  10653  modqsubdir  10654  modqeqmodmin  10655  modsumfzodifsn  10657  addmodlteq  10659  frecuzrdgsuctlem  10684  uzsinds  10705  seqeq3  10713  iseqvalcbv  10720  seq3val  10721  seqvalcd  10722  seqf  10725  seq3p1  10726  seqovcd  10728  seqp1cd  10731  seq3m1  10734  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord2  10747  ser3mono  10748  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3caopr2  10754  seqcaopr2g  10755  seq3caopr  10756  seqcaoprg  10757  seqf1oglem2a  10779  seqf1oglem2  10781  seq3id2  10787  seq3homo  10788  seq3z  10789  seqhomog  10791  exp3vallem  10801  exp3val  10802  expp1  10807  expnegap0  10808  expineg2  10809  expn1ap0  10810  expm1t  10828  1exp  10829  expnegzap  10834  mulexpzap  10840  expadd  10842  expaddzaplem  10843  expaddzap  10844  expmul  10845  expmulzap  10846  m1expeven  10847  expsubap  10848  expp1zap  10849  expm1ap  10850  expdivap  10851  iexpcyc  10905  subsq2  10908  binom2  10912  binom21  10913  binom2sub  10914  binom2sub1  10915  mulbinom2  10917  binom3  10918  zesq  10919  bernneq  10921  sqoddm1div8  10954  mulsubdivbinom2ap  10972  nn0opthlem1d  10981  nn0opthd  10983  facp1  10991  facnn2  10995  faclbnd  11002  faclbnd6  11005  bcval  11010  bccmpl  11015  bcn0  11016  bcnn  11018  bcnp1n  11020  bcm1k  11021  bcp1n  11022  bcp1nk  11023  bcval5  11024  bcp1m1  11026  bcpasc  11027  bcn2m1  11030  bcn2p1  11031  omgadd  11064  hashunlem  11066  hashunsng  11070  hashdifsn  11082  hashxp  11089  zfz1isolemsplit  11101  zfz1isolem1  11103  zfz1iso  11104  seq3coll  11105  wrdf  11118  ccatfvalfi  11168  elfzelfzccat  11176  ccatlid  11182  ccatrid  11183  ccatass  11184  ccatalpha  11189  ccatws1leng  11210  ccats1val2  11216  ccatw2s1p1g  11221  swrdval  11228  swrd00g  11229  swrdf  11235  swrdfv2  11243  swrdwrdsymbg  11244  swrdspsleq  11247  swrds1  11248  swrdlsw  11249  ccatswrd  11250  swrdccat2  11251  pfxmpt  11260  pfxfv  11264  pfxeq  11276  pfxsuff1eqwrdeq  11279  ccatpfx  11281  pfxccat1  11282  swrdswrd  11285  pfxswrd  11286  swrdpfx  11287  pfxpfx  11288  pfxlswccat  11293  ccats1pfxeq  11294  ccats1pfxeqrex  11295  ccatopth2  11297  cats1un  11301  wrdind  11302  wrd2ind  11303  swrdccatfn  11304  swrdccatin1  11305  pfxccatin12lem4  11306  swrdccatin2  11309  pfxccatin12lem2c  11310  pfxccatin12lem2  11311  pfxccatin12  11313  swrdccat  11315  swrdccat3blem  11319  swrdccat3b  11320  swrdccatin2d  11324  pfxccatin12d  11325  reuccatpfxs1lem  11326  reuccatpfxs1  11327  shftcan1  11394  shftcan2  11395  cjval  11405  cjth  11406  crre  11417  replim  11419  remim  11420  reim0b  11422  rereb  11423  mulreap  11424  cjreb  11426  recj  11427  reneg  11428  readd  11429  resub  11430  remullem  11431  imcj  11435  imneg  11436  imadd  11437  imsub  11438  cjcj  11443  cjadd  11444  ipcnval  11446  cjmulrcl  11447  cjneg  11450  addcj  11451  cjsub  11452  cnrecnv  11470  caucvgrelemcau  11540  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniqlem  11554  resqrexlemover  11570  resqrexlemlo  11573  resqrexlemcalc1  11574  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemcvg  11579  absneg  11610  abscj  11612  sqabsadd  11615  sqabssub  11616  absmul  11629  absid  11631  absre  11637  absresq  11638  absexpzap  11640  recvalap  11657  abstri  11664  abs2dif2  11667  recan  11669  cau3lem  11674  amgm2  11678  bdtrilem  11799  xrmaxadd  11821  xrbdtri  11836  climaddc1  11889  climsubc1  11892  climcvg1nlem  11909  serf0  11912  summodclem3  11940  summodclem2a  11941  summodc  11943  fsumsplitsn  11970  fsumm1  11976  fsumsplitsnun  11979  fsump1  11980  isummulc2  11986  fsumrev  12003  fisum0diag2  12007  fsummulc2  12008  fsumsub  12012  fsumabs  12025  telfsumo  12026  fsumparts  12030  fsumrelem  12031  fsumiun  12037  binomlem  12043  binom  12044  binom1p  12045  binom11  12046  binom1dif  12047  bcxmas  12049  isumsplit  12051  isum1p  12052  divcnv  12057  arisum2  12059  trireciplem  12060  trirecip  12061  geolim  12071  georeclim  12073  geo2sum  12074  geo2lim  12076  geoisum1c  12080  0.999...  12081  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratz  12092  mertenslem2  12096  mertensabs  12097  clim2prod  12099  prodfrecap  12106  prodfdivap  12107  prodmodclem3  12135  prodmodclem2a  12136  fprodm1  12158  fprodp1  12160  fprodunsn  12164  fprodfac  12175  fprodeq0  12177  fprodconst  12180  fprodrec  12189  fproddivap  12190  fprodsplitsn  12193  ege2le3  12231  efaddlem  12234  efsub  12241  efexp  12242  eftlub  12250  efsep  12251  effsumlt  12252  ef4p  12254  tanval3ap  12274  resinval  12275  recosval  12276  efi4p  12277  efival  12292  efmival  12293  efeul  12294  sinadd  12296  cosadd  12297  tanaddap  12299  sinsub  12300  cossub  12301  sincossq  12308  sin2t  12309  cos2t  12310  cos2tsin  12311  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos12dec  12328  absef  12330  absefib  12331  efieq1re  12332  demoivreALT  12334  eirraplem  12337  dvdsexp  12421  oexpneg  12437  opeo  12457  omeo  12458  m1exp1  12461  flodddiv4  12496  flodddiv4t2lthalf  12499  bitsval  12503  bitsp1  12511  bitsinv1lem  12521  bitsinv1  12522  divgcdnnr  12546  gcdaddm  12554  gcdadd  12555  gcdid  12556  modgcd  12561  gcdmultipled  12563  dvdsgcdidd  12564  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  bezoutlemex  12571  bezoutlembz  12574  absmulgcd  12587  gcdmultiple  12590  gcdmultiplez  12591  rpmulgcd  12596  rplpwr  12597  eucalginv  12627  eucalg  12630  lcmneg  12645  lcmgcdlem  12648  lcmgcd  12649  lcmid  12651  lcm1  12652  mulgcddvds  12665  qredeq  12667  divgcdcoprmex  12673  prmind2  12691  rpexp1i  12725  pw2dvdslemn  12736  pw2dvdseulemle  12738  pw2dvdseu  12739  oddpwdclemxy  12740  oddpwdclemdvds  12741  oddpwdclemndvds  12742  oddpwdclemdc  12744  2sqpwodd  12747  nn0gcdsq  12771  phiprmpw  12793  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  fermltl  12805  prmdiv  12806  hashgcdlem  12809  odzdvds  12817  vfermltl  12823  modprm0  12826  nnnn0modprm0  12827  modprmn0modprm0  12828  coprimeprodsq  12829  pythagtriplem1  12837  pythagtriplem4  12840  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  pythagtriplem18  12853  pythagtrip  12855  pcpremul  12865  pceu  12867  pczpre  12869  pcdiv  12874  pcqmul  12875  pcqdiv  12879  pcexp  12881  pcxqcl  12884  pczdvds  12886  pczndvds  12888  pczndvds2  12890  pcid  12896  pcneg  12897  pcdvdstr  12899  pcgcd1  12900  pcgcd  12901  pc2dvds  12902  pcaddlem  12911  pcadd  12912  pcadd2  12913  pcmpt  12915  pcmpt2  12916  fldivp1  12920  pcfac  12922  pcbc  12923  expnprm  12925  prmpwdvds  12927  pockthlem  12928  pockthi  12930  4sqlem7  12956  4sqlem9  12958  4sqlem10  12959  4sqlem2  12961  4sqlem3  12962  4sqlem4  12964  mul4sqlem  12965  4sqlem11  12973  4sqlem16  12978  4sqlem17  12979  4sqlem19  12981  setscomd  13122  ressvalsets  13146  strressid  13153  ressval3d  13154  ressinbasd  13156  ressressg  13157  ressabsg  13158  grpinvalem  13467  grpinva  13468  grprida  13469  isnsgrp  13488  sgrpass  13490  sgrp1  13493  sgrppropd  13495  prdssgrpd  13497  mnd32g  13509  mnd4g  13511  mndpropd  13522  prdsidlem  13529  prdsmndd  13530  imasmnd2  13534  mhmex  13544  mhmlin  13549  gsumwmhm  13580  grprcan  13619  grpsubval  13628  grpinvid2  13635  grpasscan2  13646  grpsubinv  13655  grpinvadd  13660  grpsubid1  13667  grpsubadd0sub  13669  grpsubadd  13670  grpsubsub  13671  grpaddsubass  13672  grppncan  13673  grpnnncan2  13679  grpsubpropd2  13687  imasgrp2  13696  mhmlem  13700  mhmid  13701  mhmmnd  13702  ghmgrp  13704  mulgnn0gsum  13714  mulgnnp1  13716  mulgaddcomlem  13731  mulgaddcom  13732  mulginvinv  13734  mulgnn0dir  13738  mulgdirlem  13739  mulgp1  13741  mulgneg2  13742  mulgnn0ass  13744  mulgass  13745  mulgmodid  13747  mulgsubdir  13748  nmzsubg  13796  0nsg  13800  eqger  13810  qussub  13823  ghmlin  13834  ghmsub  13837  conjghm  13862  ablsub4  13899  abladdsub4  13900  ablsubsub4  13905  ablsub32  13908  ablnnncan  13909  gsumfzmptfidmadd2  13926  gsumfzconst  13927  gsumfzmhm2  13930  gsumfzsnfd  13931  mgpress  13943  rngass  13951  rngdi  13952  rngdir  13953  rngrz  13958  rngmneg2  13960  rngsubdi  13963  rngsubdir  13964  rngpropd  13967  imasrng  13968  srgass  13983  srgpcomp  14002  srgpcompp  14003  srgpcomppsc  14004  srg1expzeq1  14007  ringpropd  14050  ringrz  14056  ringnegr  14064  ringmneg2  14066  ringsubdi  14068  ringsubdir  14069  ring1  14071  imasring  14076  opprrng  14089  opprring  14091  mulgass3  14097  dvdsrd  14107  unitgrp  14129  invrfvald  14135  dvr1  14151  dvrass  14152  dvrcan1  14153  dvrcan3  14154  rdivmuldivd  14157  subrginv  14250  subrgdv  14251  resrhm2b  14262  islmod  14304  lmodlema  14305  islmodd  14306  lmodvs0  14335  lmodvneg1  14343  lmodvsubval2  14355  lmodsubvs  14356  lmodsubdi  14357  lmodsubdir  14358  lmodprop2d  14361  rmodislmodlem  14363  rmodislmod  14364  lsssn0  14383  sraval  14450  cnfldsub  14588  gsumfzfsumlem0  14599  gsumfzfsumlemm  14600  mulgrhm  14622  mulgrhm2  14623  znval  14649  znval2  14651  znunit  14672  psrval  14679  mplvalcoe  14703  mplval2g  14708  restabs  14898  cnprcl2k  14929  cnrest2r  14960  ispsmet  15046  psmettri2  15051  psmetsym  15052  ismet  15067  isxmet  15068  xmettri2  15084  xmetsym  15091  xmettri3  15097  mettri3  15098  xblss2ps  15127  xblss2  15128  comet  15222  xmetxp  15230  xmetxpbl  15231  txmetcnp  15241  fsumcncntop  15290  cncfi  15301  divcncfap  15337  limccl  15382  ellimc3apf  15383  limccnpcntop  15398  limccnp2lem  15399  reldvg  15402  dvfvalap  15404  eldvap  15405  dvcj  15432  dvfre  15433  dvexp  15434  dvexp2  15435  dvrecap  15436  dvmptaddx  15442  dvmptmulx  15443  dvmptnegcn  15445  dvmptsubcn  15446  dvmptcjx  15447  dvmptfsum  15448  dveflem  15449  dvef  15450  plyconst  15468  plyaddlem1  15470  plymullem1  15471  plyadd  15474  plymul  15475  plycoeid3  15480  plycolemc  15481  plyco  15482  plycjlemc  15483  plycj  15484  plyrecj  15486  dvply1  15488  dvply2g  15489  sin0pilem1  15504  sin0pilem2  15505  efper  15530  sinperlem  15531  efimpi  15542  ptolemy  15547  tangtx  15561  abssinper  15569  cosq34lt1  15573  rpcxpef  15617  rpcxpp1  15629  rpcxpneg  15630  rpcxpsub  15631  rpmulcxp  15632  rpdivcxp  15634  cxpmul  15635  rpcxpmul2  15636  rpcxproot  15637  cxpcom  15661  rpabscxpbnd  15663  rplogbval  15668  rplogbreexp  15676  rplogbzexp  15677  rprelogbmulexp  15679  rprelogbdiv  15680  relogbexpap  15681  rplogbcxp  15686  rpcxplogb  15687  logbgcd1irr  15690  logbgcd1irraplemap  15692  binom4  15702  wilthlem1  15703  sgmval  15706  sgmppw  15715  1sgmprm  15717  mersenne  15720  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgslem1  15728  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsval4  15748  lgsneg  15752  lgsneg1  15753  lgsmod  15754  lgsdir2  15761  lgsdirprm  15762  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgssq2  15769  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem2  15790  gausslemma2dlem3  15791  gausslemma2dlem4  15792  gausslemma2dlem5  15794  gausslemma2dlem6  15795  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  lgsquad2lem2  15810  lgsquad2  15811  lgsquad3  15812  m1lgs  15813  2lgslem3c  15823  2lgslem3d  15824  2lgslem3d1  15828  2sqlem2  15843  2sqlem3  15845  2sqlem4  15846  2sqlem8  15851  2sqlem9  15852  2sqlem10  15853  vtxdumgrfival  16148  p1evtxdeqfi  16162  p1evtxdp1fi  16163  iswlk  16173  upgr2wlkdc  16227  wlkres  16229  trlreslem  16239  isclwwlk  16244  clwwlkccatlem  16250  clwwlknp  16267  clwwlkn1  16268  clwwlkn2  16271  clwwlkext2edg  16272  clwwlknonex2lem1  16287  clwwlknonex2lem2  16288  clwwlknonex2  16289  iseupth  16297  qdencn  16631  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trilpo  16647  apdifflemf  16650  apdiff  16652  iswomni0  16655  redcwlpolemeq1  16658  redcwlpo  16659  nconstwlpolem0  16667  nconstwlpolemgt0  16668  nconstwlpo  16670  neapmkv  16672  gfsumval  16680  gsumgfsum1  16681  gsumgfsum  16684