Theorem oveq2d 5941

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

Syntax hints:   → wi 4   = wceq 1364  (class class class)co 5925

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  csbov1g  5966  caovassg  6086  caovdig  6102  caovdirg  6105  caov32d  6108  caov4d  6112  caov42d  6114  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  addasspig  7414  mulasspig  7416  distrpig  7417  dfplpq2  7438  mulpipq2  7455  addassnqg  7466  prarloclemarch  7502  prarloclemarch2  7503  ltrnqg  7504  enq0sym  7516  addnq0mo  7531  mulnq0mo  7532  addnnnq0  7533  nq0a0  7541  distrnq0  7543  addassnq0  7546  prarloclemlo  7578  prarloclem3  7581  prarloclem5  7584  prarloclemcalc  7586  addnqprl  7613  addnqpru  7614  prmuloclemcalc  7649  mulnqprl  7652  mulnqpru  7653  distrlem4prl  7668  distrlem4pru  7669  1idprl  7674  1idpru  7675  ltexprlemloc  7691  addcanprleml  7698  addcanprlemu  7699  recexprlem1ssu  7718  ltmprr  7726  caucvgprlemcanl  7728  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlemlim  7745  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgpr  7766  caucvgprprlemell  7769  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnkeqj  7774  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexb  7791  caucvgprprlemaddq  7792  caucvgprprlem1  7793  addcmpblnr  7823  mulcmpblnrlemg  7824  addsrmo  7827  mulsrmo  7828  addsrpr  7829  mulsrpr  7830  ltsrprg  7831  recexgt0sr  7857  mulgt0sr  7862  caucvgsrlemgt1  7879  caucvgsrlemoffval  7880  caucvgsr  7886  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  suplocsr  7893  mulcnsr  7919  pitoregt0  7933  recidpirqlemcalc  7941  axmulcom  7955  axmulass  7957  axdistr  7958  ax0id  7962  axcnre  7965  recriota  7974  axcaucvglemcau  7982  axcaucvglemres  7983  mulrid  8040  adddirp1d  8070  mul32  8173  mul31  8174  add32  8202  add4  8204  add42  8205  cnegex  8221  addcan2  8224  addsubass  8253  subsub2  8271  nppcan2  8274  sub32  8277  nnncan  8278  sub4  8288  muladd  8427  subdi  8428  mul2neg  8441  submul2  8442  mulsub  8444  muls1d  8461  mulsubfacd  8462  add20  8518  recexre  8622  rereim  8630  apreap  8631  ltmul1  8636  cru  8646  apreim  8647  mulreim  8648  apadd1  8652  apneg  8655  mulap0  8698  divrecap  8732  divassap  8734  divmulasscomap  8740  divsubdirap  8752  divdivdivap  8757  divmul24ap  8760  divmuleqap  8761  divcanap6  8763  divdivap1  8767  divdivap2  8768  divsubdivap  8772  conjmulap  8773  div2negap  8779  apmul1  8832  cju  9005  nnmulcl  9028  add1p1  9258  sub1m1  9259  cnm2m1cnm3  9260  xp1d2m1eqxm1d2  9261  div4p1lem1div2  9262  un0addcl  9299  un0mulcl  9300  zaddcllemneg  9382  qapne  9730  cnref1o  9742  rexsub  9945  xnegid  9951  xaddcom  9953  xnegdi  9960  xaddass  9961  xaddass2  9962  xpncan  9963  xnpcan  9964  xleadd1a  9965  xsubge0  9973  xposdif  9974  xlesubadd  9975  xadd4d  9977  lincmb01cmp  10095  iccf1o  10096  ige3m2fz  10141  fztp  10170  fzsuc2  10171  fseq1m1p1  10187  fzm1  10192  ige2m1fz1  10201  nn0split  10228  nnsplit  10229  fzval3  10297  zpnn0elfzo1  10301  fzosplitsnm1  10302  fzosplitprm1  10327  fzoshftral  10331  rebtwn2zlemstep  10359  flhalf  10409  fldiv4lem1div2uz2  10413  modqval  10433  modqvalr  10434  modqdiffl  10444  modqfrac  10446  flqmod  10447  intqfrac  10448  zmod10  10449  modqmulnn  10451  modqvalp1  10452  modqid  10458  modqcyc  10468  modqcyc2  10469  modqmul1  10486  q2submod  10494  modqdi  10501  modqsubdir  10502  modqeqmodmin  10503  modsumfzodifsn  10505  addmodlteq  10507  frecuzrdgsuctlem  10532  uzsinds  10553  seqeq3  10561  iseqvalcbv  10568  seq3val  10569  seqvalcd  10570  seqf  10573  seq3p1  10574  seqovcd  10576  seqp1cd  10579  seq3m1  10582  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord2  10595  ser3mono  10596  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seq3caopr2  10602  seqcaopr2g  10603  seq3caopr  10604  seqcaoprg  10605  seqf1oglem2a  10627  seqf1oglem2  10629  seq3id2  10635  seq3homo  10636  seq3z  10637  seqhomog  10639  exp3vallem  10649  exp3val  10650  expp1  10655  expnegap0  10656  expineg2  10657  expn1ap0  10658  expm1t  10676  1exp  10677  expnegzap  10682  mulexpzap  10688  expadd  10690  expaddzaplem  10691  expaddzap  10692  expmul  10693  expmulzap  10694  m1expeven  10695  expsubap  10696  expp1zap  10697  expm1ap  10698  expdivap  10699  iexpcyc  10753  subsq2  10756  binom2  10760  binom21  10761  binom2sub  10762  binom2sub1  10763  mulbinom2  10765  binom3  10766  zesq  10767  bernneq  10769  sqoddm1div8  10802  mulsubdivbinom2ap  10820  nn0opthlem1d  10829  nn0opthd  10831  facp1  10839  facnn2  10843  faclbnd  10850  faclbnd6  10853  bcval  10858  bccmpl  10863  bcn0  10864  bcnn  10866  bcnp1n  10868  bcm1k  10869  bcp1n  10870  bcp1nk  10871  bcval5  10872  bcp1m1  10874  bcpasc  10875  bcn2m1  10878  bcn2p1  10879  omgadd  10911  hashunlem  10913  hashunsng  10916  hashdifsn  10928  hashxp  10935  zfz1isolemsplit  10947  zfz1isolem1  10949  zfz1iso  10950  seq3coll  10951  wrdf  10958  shftcan1  11016  shftcan2  11017  cjval  11027  cjth  11028  crre  11039  replim  11041  remim  11042  reim0b  11044  rereb  11045  mulreap  11046  cjreb  11048  recj  11049  reneg  11050  readd  11051  resub  11052  remullem  11053  imcj  11057  imneg  11058  imadd  11059  imsub  11060  cjcj  11065  cjadd  11066  ipcnval  11068  cjmulrcl  11069  cjneg  11072  addcj  11073  cjsub  11074  cnrecnv  11092  caucvgrelemcau  11162  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniqlem  11176  resqrexlemover  11192  resqrexlemlo  11195  resqrexlemcalc1  11196  resqrexlemcalc3  11198  resqrexlemnm  11200  resqrexlemcvg  11201  absneg  11232  abscj  11234  sqabsadd  11237  sqabssub  11238  absmul  11251  absid  11253  absre  11259  absresq  11260  absexpzap  11262  recvalap  11279  abstri  11286  abs2dif2  11289  recan  11291  cau3lem  11296  amgm2  11300  bdtrilem  11421  xrmaxadd  11443  xrbdtri  11458  climaddc1  11511  climsubc1  11514  climcvg1nlem  11531  serf0  11534  summodclem3  11562  summodclem2a  11563  summodc  11565  fsumsplitsn  11592  fsumm1  11598  fsumsplitsnun  11601  fsump1  11602  isummulc2  11608  fsumrev  11625  fisum0diag2  11629  fsummulc2  11630  fsumsub  11634  fsumabs  11647  telfsumo  11648  fsumparts  11652  fsumrelem  11653  fsumiun  11659  binomlem  11665  binom  11666  binom1p  11667  binom11  11668  binom1dif  11669  bcxmas  11671  isumsplit  11673  isum1p  11674  divcnv  11679  arisum2  11681  trireciplem  11682  trirecip  11683  geolim  11693  georeclim  11695  geo2sum  11696  geo2lim  11698  geoisum1c  11702  0.999...  11703  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratz  11714  mertenslem2  11718  mertensabs  11719  clim2prod  11721  prodfrecap  11728  prodfdivap  11729  prodmodclem3  11757  prodmodclem2a  11758  fprodm1  11780  fprodp1  11782  fprodunsn  11786  fprodfac  11797  fprodeq0  11799  fprodconst  11802  fprodrec  11811  fproddivap  11812  fprodsplitsn  11815  ege2le3  11853  efaddlem  11856  efsub  11863  efexp  11864  eftlub  11872  efsep  11873  effsumlt  11874  ef4p  11876  tanval3ap  11896  resinval  11897  recosval  11898  efi4p  11899  efival  11914  efmival  11915  efeul  11916  sinadd  11918  cosadd  11919  tanaddap  11921  sinsub  11922  cossub  11923  sincossq  11930  sin2t  11931  cos2t  11932  cos2tsin  11933  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  cos12dec  11950  absef  11952  absefib  11953  efieq1re  11954  demoivreALT  11956  eirraplem  11959  dvdsexp  12043  oexpneg  12059  opeo  12079  omeo  12080  m1exp1  12083  flodddiv4  12118  flodddiv4t2lthalf  12121  bitsval  12125  bitsp1  12133  bitsinv1lem  12143  bitsinv1  12144  divgcdnnr  12168  gcdaddm  12176  gcdadd  12177  gcdid  12178  modgcd  12183  gcdmultipled  12185  dvdsgcdidd  12186  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  bezoutlemex  12193  bezoutlembz  12196  absmulgcd  12209  gcdmultiple  12212  gcdmultiplez  12213  rpmulgcd  12218  rplpwr  12219  eucalginv  12249  eucalg  12252  lcmneg  12267  lcmgcdlem  12270  lcmgcd  12271  lcmid  12273  lcm1  12274  mulgcddvds  12287  qredeq  12289  divgcdcoprmex  12295  prmind2  12313  rpexp1i  12347  pw2dvdslemn  12358  pw2dvdseulemle  12360  pw2dvdseu  12361  oddpwdclemxy  12362  oddpwdclemdvds  12363  oddpwdclemndvds  12364  oddpwdclemdc  12366  2sqpwodd  12369  nn0gcdsq  12393  phiprmpw  12415  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  fermltl  12427  prmdiv  12428  hashgcdlem  12431  odzdvds  12439  vfermltl  12445  modprm0  12448  nnnn0modprm0  12449  modprmn0modprm0  12450  coprimeprodsq  12451  pythagtriplem1  12459  pythagtriplem4  12462  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem16  12473  pythagtriplem18  12475  pythagtrip  12477  pcpremul  12487  pceu  12489  pczpre  12491  pcdiv  12496  pcqmul  12497  pcqdiv  12501  pcexp  12503  pcxqcl  12506  pczdvds  12508  pczndvds  12510  pczndvds2  12512  pcid  12518  pcneg  12519  pcdvdstr  12521  pcgcd1  12522  pcgcd  12523  pc2dvds  12524  pcaddlem  12533  pcadd  12534  pcadd2  12535  pcmpt  12537  pcmpt2  12538  fldivp1  12542  pcfac  12544  pcbc  12545  expnprm  12547  prmpwdvds  12549  pockthlem  12550  pockthi  12552  4sqlem7  12578  4sqlem9  12580  4sqlem10  12581  4sqlem2  12583  4sqlem3  12584  4sqlem4  12586  mul4sqlem  12587  4sqlem11  12595  4sqlem16  12600  4sqlem17  12601  4sqlem19  12603  setscomd  12744  ressvalsets  12767  strressid  12774  ressval3d  12775  ressinbasd  12777  ressressg  12778  ressabsg  12779  grpinvalem  13087  grpinva  13088  grprida  13089  isnsgrp  13108  sgrpass  13110  sgrp1  13113  sgrppropd  13115  prdssgrpd  13117  mnd32g  13129  mnd4g  13131  mndpropd  13142  prdsidlem  13149  prdsmndd  13150  imasmnd2  13154  mhmex  13164  mhmlin  13169  gsumwmhm  13200  grprcan  13239  grpsubval  13248  grpinvid2  13255  grpasscan2  13266  grpsubinv  13275  grpinvadd  13280  grpsubid1  13287  grpsubadd0sub  13289  grpsubadd  13290  grpsubsub  13291  grpaddsubass  13292  grppncan  13293  grpnnncan2  13299  grpsubpropd2  13307  imasgrp2  13316  mhmlem  13320  mhmid  13321  mhmmnd  13322  ghmgrp  13324  mulgnn0gsum  13334  mulgnnp1  13336  mulgaddcomlem  13351  mulgaddcom  13352  mulginvinv  13354  mulgnn0dir  13358  mulgdirlem  13359  mulgp1  13361  mulgneg2  13362  mulgnn0ass  13364  mulgass  13365  mulgmodid  13367  mulgsubdir  13368  nmzsubg  13416  0nsg  13420  eqger  13430  qussub  13443  ghmlin  13454  ghmsub  13457  conjghm  13482  ablsub4  13519  abladdsub4  13520  ablsubsub4  13525  ablsub32  13528  ablnnncan  13529  gsumfzmptfidmadd2  13546  gsumfzconst  13547  gsumfzmhm2  13550  gsumfzsnfd  13551  mgpress  13563  rngass  13571  rngdi  13572  rngdir  13573  rngrz  13578  rngmneg2  13580  rngsubdi  13583  rngsubdir  13584  rngpropd  13587  imasrng  13588  srgass  13603  srgpcomp  13622  srgpcompp  13623  srgpcomppsc  13624  srg1expzeq1  13627  ringpropd  13670  ringrz  13676  ringnegr  13684  ringmneg2  13686  ringsubdi  13688  ringsubdir  13689  ring1  13691  imasring  13696  opprrng  13709  opprring  13711  mulgass3  13717  dvdsrd  13726  unitgrp  13748  invrfvald  13754  dvr1  13770  dvrass  13771  dvrcan1  13772  dvrcan3  13773  rdivmuldivd  13776  subrginv  13869  subrgdv  13870  resrhm2b  13881  islmod  13923  lmodlema  13924  islmodd  13925  lmodvs0  13954  lmodvneg1  13962  lmodvsubval2  13974  lmodsubvs  13975  lmodsubdi  13976  lmodsubdir  13977  lmodprop2d  13980  rmodislmodlem  13982  rmodislmod  13983  lsssn0  14002  sraval  14069  cnfldsub  14207  gsumfzfsumlem0  14218  gsumfzfsumlemm  14219  mulgrhm  14241  mulgrhm2  14242  znval  14268  znval2  14270  znunit  14291  psrval  14296  restabs  14495  cnprcl2k  14526  cnrest2r  14557  ispsmet  14643  psmettri2  14648  psmetsym  14649  ismet  14664  isxmet  14665  xmettri2  14681  xmetsym  14688  xmettri3  14694  mettri3  14695  xblss2ps  14724  xblss2  14725  comet  14819  xmetxp  14827  xmetxpbl  14828  txmetcnp  14838  fsumcncntop  14887  cncfi  14898  divcncfap  14934  limccl  14979  ellimc3apf  14980  limccnpcntop  14995  limccnp2lem  14996  reldvg  14999  dvfvalap  15001  eldvap  15002  dvcj  15029  dvfre  15030  dvexp  15031  dvexp2  15032  dvrecap  15033  dvmptaddx  15039  dvmptmulx  15040  dvmptnegcn  15042  dvmptsubcn  15043  dvmptcjx  15044  dvmptfsum  15045  dveflem  15046  dvef  15047  plyconst  15065  plyaddlem1  15067  plymullem1  15068  plyadd  15071  plymul  15072  plycoeid3  15077  plycolemc  15078  plyco  15079  plycjlemc  15080  plycj  15081  plyrecj  15083  dvply1  15085  dvply2g  15086  sin0pilem1  15101  sin0pilem2  15102  efper  15127  sinperlem  15128  efimpi  15139  ptolemy  15144  tangtx  15158  abssinper  15166  cosq34lt1  15170  rpcxpef  15214  rpcxpp1  15226  rpcxpneg  15227  rpcxpsub  15228  rpmulcxp  15229  rpdivcxp  15231  cxpmul  15232  rpcxpmul2  15233  rpcxproot  15234  cxpcom  15258  rpabscxpbnd  15260  rplogbval  15265  rplogbreexp  15273  rplogbzexp  15274  rprelogbmulexp  15276  rprelogbdiv  15277  relogbexpap  15278  rplogbcxp  15283  rpcxplogb  15284  logbgcd1irr  15287  logbgcd1irraplemap  15289  binom4  15299  wilthlem1  15300  sgmval  15303  sgmppw  15312  1sgmprm  15314  mersenne  15317  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgslem1  15325  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsval4  15345  lgsneg  15349  lgsneg1  15350  lgsmod  15351  lgsdir2  15358  lgsdirprm  15359  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgssq2  15366  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem2  15387  gausslemma2dlem3  15388  gausslemma2dlem4  15389  gausslemma2dlem5  15391  gausslemma2dlem6  15392  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  lgsquad2lem2  15407  lgsquad2  15408  lgsquad3  15409  m1lgs  15410  2lgslem3c  15420  2lgslem3d  15421  2lgslem3d1  15425  2sqlem2  15440  2sqlem3  15442  2sqlem4  15443  2sqlem8  15448  2sqlem9  15449  2sqlem10  15450  qdencn  15758  trilpolemclim  15767  trilpolemcl  15768  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  trilpo  15774  apdifflemf  15777  apdiff  15779  iswomni0  15782  redcwlpolemeq1  15785  redcwlpo  15786  nconstwlpolem0  15794  nconstwlpolemgt0  15795  nconstwlpo  15797  neapmkv  15799