Theorem oveq2d 5960

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

Syntax hints:   → wi 4   = wceq 1373  (class class class)co 5944

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  csbov1g  5985  caovassg  6105  caovdig  6121  caovdirg  6124  caov32d  6127  caov4d  6131  caov42d  6133  nnaass  6571  nndi  6572  nnmass  6573  nnmsucr  6574  ecovass  6731  ecoviass  6732  ecovdi  6733  ecovidi  6734  addasspig  7443  mulasspig  7445  distrpig  7446  dfplpq2  7467  mulpipq2  7484  addassnqg  7495  prarloclemarch  7531  prarloclemarch2  7532  ltrnqg  7533  enq0sym  7545  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  nq0a0  7570  distrnq0  7572  addassnq0  7575  prarloclemlo  7607  prarloclem3  7610  prarloclem5  7613  prarloclemcalc  7615  addnqprl  7642  addnqpru  7643  prmuloclemcalc  7678  mulnqprl  7681  mulnqpru  7682  distrlem4prl  7697  distrlem4pru  7698  1idprl  7703  1idpru  7704  ltexprlemloc  7720  addcanprleml  7727  addcanprlemu  7728  recexprlem1ssu  7747  ltmprr  7755  caucvgprlemcanl  7757  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlemlim  7774  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexb  7820  caucvgprprlemaddq  7821  caucvgprprlem1  7822  addcmpblnr  7852  mulcmpblnrlemg  7853  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  ltsrprg  7860  recexgt0sr  7886  mulgt0sr  7891  caucvgsrlemgt1  7908  caucvgsrlemoffval  7909  caucvgsr  7915  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  suplocsr  7922  mulcnsr  7948  pitoregt0  7962  recidpirqlemcalc  7970  axmulcom  7984  axmulass  7986  axdistr  7987  ax0id  7991  axcnre  7994  recriota  8003  axcaucvglemcau  8011  axcaucvglemres  8012  mulrid  8069  adddirp1d  8099  mul32  8202  mul31  8203  add32  8231  add4  8233  add42  8234  cnegex  8250  addcan2  8253  addsubass  8282  subsub2  8300  nppcan2  8303  sub32  8306  nnncan  8307  sub4  8317  muladd  8456  subdi  8457  mul2neg  8470  submul2  8471  mulsub  8473  muls1d  8490  mulsubfacd  8491  add20  8547  recexre  8651  rereim  8659  apreap  8660  ltmul1  8665  cru  8675  apreim  8676  mulreim  8677  apadd1  8681  apneg  8684  mulap0  8727  divrecap  8761  divassap  8763  divmulasscomap  8769  divsubdirap  8781  divdivdivap  8786  divmul24ap  8789  divmuleqap  8790  divcanap6  8792  divdivap1  8796  divdivap2  8797  divsubdivap  8801  conjmulap  8802  div2negap  8808  apmul1  8861  cju  9034  nnmulcl  9057  add1p1  9287  sub1m1  9288  cnm2m1cnm3  9289  xp1d2m1eqxm1d2  9290  div4p1lem1div2  9291  un0addcl  9328  un0mulcl  9329  zaddcllemneg  9411  qapne  9760  cnref1o  9772  rexsub  9975  xnegid  9981  xaddcom  9983  xnegdi  9990  xaddass  9991  xaddass2  9992  xpncan  9993  xnpcan  9994  xleadd1a  9995  xsubge0  10003  xposdif  10004  xlesubadd  10005  xadd4d  10007  lincmb01cmp  10125  iccf1o  10126  ige3m2fz  10171  fztp  10200  fzsuc2  10201  fseq1m1p1  10217  fzm1  10222  ige2m1fz1  10231  nn0split  10258  nnsplit  10259  fzo0addelr  10318  elfzoext  10321  fzval3  10333  zpnn0elfzo1  10337  fzosplitsnm1  10338  fzosplitprm1  10363  fzoshftral  10367  rebtwn2zlemstep  10395  flhalf  10445  fldiv4lem1div2uz2  10449  modqval  10469  modqvalr  10470  modqdiffl  10480  modqfrac  10482  flqmod  10483  intqfrac  10484  zmod10  10485  modqmulnn  10487  modqvalp1  10488  modqid  10494  modqcyc  10504  modqcyc2  10505  modqmul1  10522  q2submod  10530  modqdi  10537  modqsubdir  10538  modqeqmodmin  10539  modsumfzodifsn  10541  addmodlteq  10543  frecuzrdgsuctlem  10568  uzsinds  10589  seqeq3  10597  iseqvalcbv  10604  seq3val  10605  seqvalcd  10606  seqf  10609  seq3p1  10610  seqovcd  10612  seqp1cd  10615  seq3m1  10618  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord2  10631  ser3mono  10632  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seq3caopr2  10638  seqcaopr2g  10639  seq3caopr  10640  seqcaoprg  10641  seqf1oglem2a  10663  seqf1oglem2  10665  seq3id2  10671  seq3homo  10672  seq3z  10673  seqhomog  10675  exp3vallem  10685  exp3val  10686  expp1  10691  expnegap0  10692  expineg2  10693  expn1ap0  10694  expm1t  10712  1exp  10713  expnegzap  10718  mulexpzap  10724  expadd  10726  expaddzaplem  10727  expaddzap  10728  expmul  10729  expmulzap  10730  m1expeven  10731  expsubap  10732  expp1zap  10733  expm1ap  10734  expdivap  10735  iexpcyc  10789  subsq2  10792  binom2  10796  binom21  10797  binom2sub  10798  binom2sub1  10799  mulbinom2  10801  binom3  10802  zesq  10803  bernneq  10805  sqoddm1div8  10838  mulsubdivbinom2ap  10856  nn0opthlem1d  10865  nn0opthd  10867  facp1  10875  facnn2  10879  faclbnd  10886  faclbnd6  10889  bcval  10894  bccmpl  10899  bcn0  10900  bcnn  10902  bcnp1n  10904  bcm1k  10905  bcp1n  10906  bcp1nk  10907  bcval5  10908  bcp1m1  10910  bcpasc  10911  bcn2m1  10914  bcn2p1  10915  omgadd  10947  hashunlem  10949  hashunsng  10952  hashdifsn  10964  hashxp  10971  zfz1isolemsplit  10983  zfz1isolem1  10985  zfz1iso  10986  seq3coll  10987  wrdf  11000  ccatfvalfi  11048  elfzelfzccat  11056  ccatlid  11062  ccatrid  11063  ccatass  11064  ccatws1leng  11088  ccats1val2  11092  swrdval  11101  swrd00g  11102  swrdf  11108  swrdfv2  11116  swrdwrdsymbg  11117  swrdspsleq  11120  swrds1  11121  swrdlsw  11122  ccatswrd  11123  swrdccat2  11124  shftcan1  11145  shftcan2  11146  cjval  11156  cjth  11157  crre  11168  replim  11170  remim  11171  reim0b  11173  rereb  11174  mulreap  11175  cjreb  11177  recj  11178  reneg  11179  readd  11180  resub  11181  remullem  11182  imcj  11186  imneg  11187  imadd  11188  imsub  11189  cjcj  11194  cjadd  11195  ipcnval  11197  cjmulrcl  11198  cjneg  11201  addcj  11202  cjsub  11203  cnrecnv  11221  caucvgrelemcau  11291  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniqlem  11305  resqrexlemover  11321  resqrexlemlo  11324  resqrexlemcalc1  11325  resqrexlemcalc3  11327  resqrexlemnm  11329  resqrexlemcvg  11330  absneg  11361  abscj  11363  sqabsadd  11366  sqabssub  11367  absmul  11380  absid  11382  absre  11388  absresq  11389  absexpzap  11391  recvalap  11408  abstri  11415  abs2dif2  11418  recan  11420  cau3lem  11425  amgm2  11429  bdtrilem  11550  xrmaxadd  11572  xrbdtri  11587  climaddc1  11640  climsubc1  11643  climcvg1nlem  11660  serf0  11663  summodclem3  11691  summodclem2a  11692  summodc  11694  fsumsplitsn  11721  fsumm1  11727  fsumsplitsnun  11730  fsump1  11731  isummulc2  11737  fsumrev  11754  fisum0diag2  11758  fsummulc2  11759  fsumsub  11763  fsumabs  11776  telfsumo  11777  fsumparts  11781  fsumrelem  11782  fsumiun  11788  binomlem  11794  binom  11795  binom1p  11796  binom11  11797  binom1dif  11798  bcxmas  11800  isumsplit  11802  isum1p  11803  divcnv  11808  arisum2  11810  trireciplem  11811  trirecip  11812  geolim  11822  georeclim  11824  geo2sum  11825  geo2lim  11827  geoisum1c  11831  0.999...  11832  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratz  11843  mertenslem2  11847  mertensabs  11848  clim2prod  11850  prodfrecap  11857  prodfdivap  11858  prodmodclem3  11886  prodmodclem2a  11887  fprodm1  11909  fprodp1  11911  fprodunsn  11915  fprodfac  11926  fprodeq0  11928  fprodconst  11931  fprodrec  11940  fproddivap  11941  fprodsplitsn  11944  ege2le3  11982  efaddlem  11985  efsub  11992  efexp  11993  eftlub  12001  efsep  12002  effsumlt  12003  ef4p  12005  tanval3ap  12025  resinval  12026  recosval  12027  efi4p  12028  efival  12043  efmival  12044  efeul  12045  sinadd  12047  cosadd  12048  tanaddap  12050  sinsub  12051  cossub  12052  sincossq  12059  sin2t  12060  cos2t  12061  cos2tsin  12062  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  cos12dec  12079  absef  12081  absefib  12082  efieq1re  12083  demoivreALT  12085  eirraplem  12088  dvdsexp  12172  oexpneg  12188  opeo  12208  omeo  12209  m1exp1  12212  flodddiv4  12247  flodddiv4t2lthalf  12250  bitsval  12254  bitsp1  12262  bitsinv1lem  12272  bitsinv1  12273  divgcdnnr  12297  gcdaddm  12305  gcdadd  12306  gcdid  12307  modgcd  12312  gcdmultipled  12314  dvdsgcdidd  12315  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  bezoutlemex  12322  bezoutlembz  12325  absmulgcd  12338  gcdmultiple  12341  gcdmultiplez  12342  rpmulgcd  12347  rplpwr  12348  eucalginv  12378  eucalg  12381  lcmneg  12396  lcmgcdlem  12399  lcmgcd  12400  lcmid  12402  lcm1  12403  mulgcddvds  12416  qredeq  12418  divgcdcoprmex  12424  prmind2  12442  rpexp1i  12476  pw2dvdslemn  12487  pw2dvdseulemle  12489  pw2dvdseu  12490  oddpwdclemxy  12491  oddpwdclemdvds  12492  oddpwdclemndvds  12493  oddpwdclemdc  12495  2sqpwodd  12498  nn0gcdsq  12522  phiprmpw  12544  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  fermltl  12556  prmdiv  12557  hashgcdlem  12560  odzdvds  12568  vfermltl  12574  modprm0  12577  nnnn0modprm0  12578  modprmn0modprm0  12579  coprimeprodsq  12580  pythagtriplem1  12588  pythagtriplem4  12591  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem16  12602  pythagtriplem18  12604  pythagtrip  12606  pcpremul  12616  pceu  12618  pczpre  12620  pcdiv  12625  pcqmul  12626  pcqdiv  12630  pcexp  12632  pcxqcl  12635  pczdvds  12637  pczndvds  12639  pczndvds2  12641  pcid  12647  pcneg  12648  pcdvdstr  12650  pcgcd1  12651  pcgcd  12652  pc2dvds  12653  pcaddlem  12662  pcadd  12663  pcadd2  12664  pcmpt  12666  pcmpt2  12667  fldivp1  12671  pcfac  12673  pcbc  12674  expnprm  12676  prmpwdvds  12678  pockthlem  12679  pockthi  12681  4sqlem7  12707  4sqlem9  12709  4sqlem10  12710  4sqlem2  12712  4sqlem3  12713  4sqlem4  12715  mul4sqlem  12716  4sqlem11  12724  4sqlem16  12729  4sqlem17  12730  4sqlem19  12732  setscomd  12873  ressvalsets  12896  strressid  12903  ressval3d  12904  ressinbasd  12906  ressressg  12907  ressabsg  12908  grpinvalem  13217  grpinva  13218  grprida  13219  isnsgrp  13238  sgrpass  13240  sgrp1  13243  sgrppropd  13245  prdssgrpd  13247  mnd32g  13259  mnd4g  13261  mndpropd  13272  prdsidlem  13279  prdsmndd  13280  imasmnd2  13284  mhmex  13294  mhmlin  13299  gsumwmhm  13330  grprcan  13369  grpsubval  13378  grpinvid2  13385  grpasscan2  13396  grpsubinv  13405  grpinvadd  13410  grpsubid1  13417  grpsubadd0sub  13419  grpsubadd  13420  grpsubsub  13421  grpaddsubass  13422  grppncan  13423  grpnnncan2  13429  grpsubpropd2  13437  imasgrp2  13446  mhmlem  13450  mhmid  13451  mhmmnd  13452  ghmgrp  13454  mulgnn0gsum  13464  mulgnnp1  13466  mulgaddcomlem  13481  mulgaddcom  13482  mulginvinv  13484  mulgnn0dir  13488  mulgdirlem  13489  mulgp1  13491  mulgneg2  13492  mulgnn0ass  13494  mulgass  13495  mulgmodid  13497  mulgsubdir  13498  nmzsubg  13546  0nsg  13550  eqger  13560  qussub  13573  ghmlin  13584  ghmsub  13587  conjghm  13612  ablsub4  13649  abladdsub4  13650  ablsubsub4  13655  ablsub32  13658  ablnnncan  13659  gsumfzmptfidmadd2  13676  gsumfzconst  13677  gsumfzmhm2  13680  gsumfzsnfd  13681  mgpress  13693  rngass  13701  rngdi  13702  rngdir  13703  rngrz  13708  rngmneg2  13710  rngsubdi  13713  rngsubdir  13714  rngpropd  13717  imasrng  13718  srgass  13733  srgpcomp  13752  srgpcompp  13753  srgpcomppsc  13754  srg1expzeq1  13757  ringpropd  13800  ringrz  13806  ringnegr  13814  ringmneg2  13816  ringsubdi  13818  ringsubdir  13819  ring1  13821  imasring  13826  opprrng  13839  opprring  13841  mulgass3  13847  dvdsrd  13856  unitgrp  13878  invrfvald  13884  dvr1  13900  dvrass  13901  dvrcan1  13902  dvrcan3  13903  rdivmuldivd  13906  subrginv  13999  subrgdv  14000  resrhm2b  14011  islmod  14053  lmodlema  14054  islmodd  14055  lmodvs0  14084  lmodvneg1  14092  lmodvsubval2  14104  lmodsubvs  14105  lmodsubdi  14106  lmodsubdir  14107  lmodprop2d  14110  rmodislmodlem  14112  rmodislmod  14113  lsssn0  14132  sraval  14199  cnfldsub  14337  gsumfzfsumlem0  14348  gsumfzfsumlemm  14349  mulgrhm  14371  mulgrhm2  14372  znval  14398  znval2  14400  znunit  14421  psrval  14428  mplvalcoe  14452  mplval2g  14457  restabs  14647  cnprcl2k  14678  cnrest2r  14709  ispsmet  14795  psmettri2  14800  psmetsym  14801  ismet  14816  isxmet  14817  xmettri2  14833  xmetsym  14840  xmettri3  14846  mettri3  14847  xblss2ps  14876  xblss2  14877  comet  14971  xmetxp  14979  xmetxpbl  14980  txmetcnp  14990  fsumcncntop  15039  cncfi  15050  divcncfap  15086  limccl  15131  ellimc3apf  15132  limccnpcntop  15147  limccnp2lem  15148  reldvg  15151  dvfvalap  15153  eldvap  15154  dvcj  15181  dvfre  15182  dvexp  15183  dvexp2  15184  dvrecap  15185  dvmptaddx  15191  dvmptmulx  15192  dvmptnegcn  15194  dvmptsubcn  15195  dvmptcjx  15196  dvmptfsum  15197  dveflem  15198  dvef  15199  plyconst  15217  plyaddlem1  15219  plymullem1  15220  plyadd  15223  plymul  15224  plycoeid3  15229  plycolemc  15230  plyco  15231  plycjlemc  15232  plycj  15233  plyrecj  15235  dvply1  15237  dvply2g  15238  sin0pilem1  15253  sin0pilem2  15254  efper  15279  sinperlem  15280  efimpi  15291  ptolemy  15296  tangtx  15310  abssinper  15318  cosq34lt1  15322  rpcxpef  15366  rpcxpp1  15378  rpcxpneg  15379  rpcxpsub  15380  rpmulcxp  15381  rpdivcxp  15383  cxpmul  15384  rpcxpmul2  15385  rpcxproot  15386  cxpcom  15410  rpabscxpbnd  15412  rplogbval  15417  rplogbreexp  15425  rplogbzexp  15426  rprelogbmulexp  15428  rprelogbdiv  15429  relogbexpap  15430  rplogbcxp  15435  rpcxplogb  15436  logbgcd1irr  15439  logbgcd1irraplemap  15441  binom4  15451  wilthlem1  15452  sgmval  15455  sgmppw  15464  1sgmprm  15466  mersenne  15469  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgslem1  15477  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsval4  15497  lgsneg  15501  lgsneg1  15502  lgsmod  15503  lgsdir2  15510  lgsdirprm  15511  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgssq2  15518  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem2  15539  gausslemma2dlem3  15540  gausslemma2dlem4  15541  gausslemma2dlem5  15543  gausslemma2dlem6  15544  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  lgsquad2lem2  15559  lgsquad2  15560  lgsquad3  15561  m1lgs  15562  2lgslem3c  15572  2lgslem3d  15573  2lgslem3d1  15577  2sqlem2  15592  2sqlem3  15594  2sqlem4  15595  2sqlem8  15600  2sqlem9  15601  2sqlem10  15602  qdencn  15966  trilpolemclim  15975  trilpolemcl  15976  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  trilpo  15982  apdifflemf  15985  apdiff  15987  iswomni0  15990  redcwlpolemeq1  15993  redcwlpo  15994  nconstwlpolem0  16002  nconstwlpolemgt0  16003  nconstwlpo  16005  neapmkv  16007