Theorem oveq2d 5935

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  csbov1g  5959  caovassg  6079  caovdig  6095  caovdirg  6098  caov32d  6101  caov4d  6105  caov42d  6107  nnaass  6540  nndi  6541  nnmass  6542  nnmsucr  6543  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  addasspig  7392  mulasspig  7394  distrpig  7395  dfplpq2  7416  mulpipq2  7433  addassnqg  7444  prarloclemarch  7480  prarloclemarch2  7481  ltrnqg  7482  enq0sym  7494  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  nq0a0  7519  distrnq0  7521  addassnq0  7524  prarloclemlo  7556  prarloclem3  7559  prarloclem5  7562  prarloclemcalc  7564  addnqprl  7591  addnqpru  7592  prmuloclemcalc  7627  mulnqprl  7630  mulnqpru  7631  distrlem4prl  7646  distrlem4pru  7647  1idprl  7652  1idpru  7653  ltexprlemloc  7669  addcanprleml  7676  addcanprlemu  7677  recexprlem1ssu  7696  ltmprr  7704  caucvgprlemcanl  7706  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlemlim  7723  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexb  7769  caucvgprprlemaddq  7770  caucvgprprlem1  7771  addcmpblnr  7801  mulcmpblnrlemg  7802  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  ltsrprg  7809  recexgt0sr  7835  mulgt0sr  7840  caucvgsrlemgt1  7857  caucvgsrlemoffval  7858  caucvgsr  7864  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  suplocsr  7871  mulcnsr  7897  pitoregt0  7911  recidpirqlemcalc  7919  axmulcom  7933  axmulass  7935  axdistr  7936  ax0id  7940  axcnre  7943  recriota  7952  axcaucvglemcau  7960  axcaucvglemres  7961  mulrid  8018  adddirp1d  8048  mul32  8151  mul31  8152  add32  8180  add4  8182  add42  8183  cnegex  8199  addcan2  8202  addsubass  8231  subsub2  8249  nppcan2  8252  sub32  8255  nnncan  8256  sub4  8266  muladd  8405  subdi  8406  mul2neg  8419  submul2  8420  mulsub  8422  mulsubfacd  8439  add20  8495  recexre  8599  rereim  8607  apreap  8608  ltmul1  8613  cru  8623  apreim  8624  mulreim  8625  apadd1  8629  apneg  8632  mulap0  8675  divrecap  8709  divassap  8711  divmulasscomap  8717  divsubdirap  8729  divdivdivap  8734  divmul24ap  8737  divmuleqap  8738  divcanap6  8740  divdivap1  8744  divdivap2  8745  divsubdivap  8749  conjmulap  8750  div2negap  8756  apmul1  8809  cju  8982  nnmulcl  9005  add1p1  9235  sub1m1  9236  cnm2m1cnm3  9237  xp1d2m1eqxm1d2  9238  div4p1lem1div2  9239  un0addcl  9276  un0mulcl  9277  zaddcllemneg  9359  qapne  9707  cnref1o  9719  rexsub  9922  xnegid  9928  xaddcom  9930  xnegdi  9937  xaddass  9938  xaddass2  9939  xpncan  9940  xnpcan  9941  xleadd1a  9942  xsubge0  9950  xposdif  9951  xlesubadd  9952  xadd4d  9954  lincmb01cmp  10072  iccf1o  10073  ige3m2fz  10118  fztp  10147  fzsuc2  10148  fseq1m1p1  10164  fzm1  10169  ige2m1fz1  10178  nn0split  10205  nnsplit  10206  fzval3  10274  zpnn0elfzo1  10278  fzosplitsnm1  10279  fzosplitprm1  10304  fzoshftral  10308  rebtwn2zlemstep  10324  flhalf  10374  fldiv4lem1div2uz2  10378  modqval  10398  modqvalr  10399  modqdiffl  10409  modqfrac  10411  flqmod  10412  intqfrac  10413  zmod10  10414  modqmulnn  10416  modqvalp1  10417  modqid  10423  modqcyc  10433  modqcyc2  10434  modqmul1  10451  q2submod  10459  modqdi  10466  modqsubdir  10467  modqeqmodmin  10468  modsumfzodifsn  10470  addmodlteq  10472  frecuzrdgsuctlem  10497  uzsinds  10518  seqeq3  10526  iseqvalcbv  10533  seq3val  10534  seqvalcd  10535  seqf  10538  seq3p1  10539  seqovcd  10541  seqp1cd  10544  seq3m1  10547  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord2  10560  ser3mono  10561  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seq3caopr2  10567  seqcaopr2g  10568  seq3caopr  10569  seqcaoprg  10570  seqf1oglem2a  10592  seqf1oglem2  10594  seq3id2  10600  seq3homo  10601  seq3z  10602  seqhomog  10604  exp3vallem  10614  exp3val  10615  expp1  10620  expnegap0  10621  expineg2  10622  expn1ap0  10623  expm1t  10641  1exp  10642  expnegzap  10647  mulexpzap  10653  expadd  10655  expaddzaplem  10656  expaddzap  10657  expmul  10658  expmulzap  10659  m1expeven  10660  expsubap  10661  expp1zap  10662  expm1ap  10663  expdivap  10664  iexpcyc  10718  subsq2  10721  binom2  10725  binom21  10726  binom2sub  10727  binom2sub1  10728  mulbinom2  10730  binom3  10731  zesq  10732  bernneq  10734  sqoddm1div8  10767  mulsubdivbinom2ap  10785  nn0opthlem1d  10794  nn0opthd  10796  facp1  10804  facnn2  10808  faclbnd  10815  faclbnd6  10818  bcval  10823  bccmpl  10828  bcn0  10829  bcnn  10831  bcnp1n  10833  bcm1k  10834  bcp1n  10835  bcp1nk  10836  bcval5  10837  bcp1m1  10839  bcpasc  10840  bcn2m1  10843  bcn2p1  10844  omgadd  10876  hashunlem  10878  hashunsng  10881  hashdifsn  10893  hashxp  10900  zfz1isolemsplit  10912  zfz1isolem1  10914  zfz1iso  10915  seq3coll  10916  wrdf  10923  shftcan1  10981  shftcan2  10982  cjval  10992  cjth  10993  crre  11004  replim  11006  remim  11007  reim0b  11009  rereb  11010  mulreap  11011  cjreb  11013  recj  11014  reneg  11015  readd  11016  resub  11017  remullem  11018  imcj  11022  imneg  11023  imadd  11024  imsub  11025  cjcj  11030  cjadd  11031  ipcnval  11033  cjmulrcl  11034  cjneg  11037  addcj  11038  cjsub  11039  cnrecnv  11057  caucvgrelemcau  11127  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniqlem  11141  resqrexlemover  11157  resqrexlemlo  11160  resqrexlemcalc1  11161  resqrexlemcalc3  11163  resqrexlemnm  11165  resqrexlemcvg  11166  absneg  11197  abscj  11199  sqabsadd  11202  sqabssub  11203  absmul  11216  absid  11218  absre  11224  absresq  11225  absexpzap  11227  recvalap  11244  abstri  11251  abs2dif2  11254  recan  11256  cau3lem  11261  amgm2  11265  bdtrilem  11385  xrmaxadd  11407  xrbdtri  11422  climaddc1  11475  climsubc1  11478  climcvg1nlem  11495  serf0  11498  summodclem3  11526  summodclem2a  11527  summodc  11529  fsumsplitsn  11556  fsumm1  11562  fsumsplitsnun  11565  fsump1  11566  isummulc2  11572  fsumrev  11589  fisum0diag2  11593  fsummulc2  11594  fsumsub  11598  fsumabs  11611  telfsumo  11612  fsumparts  11616  fsumrelem  11617  fsumiun  11623  binomlem  11629  binom  11630  binom1p  11631  binom11  11632  binom1dif  11633  bcxmas  11635  isumsplit  11637  isum1p  11638  divcnv  11643  arisum2  11645  trireciplem  11646  trirecip  11647  geolim  11657  georeclim  11659  geo2sum  11660  geo2lim  11662  geoisum1c  11666  0.999...  11667  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratz  11678  mertenslem2  11682  mertensabs  11683  clim2prod  11685  prodfrecap  11692  prodfdivap  11693  prodmodclem3  11721  prodmodclem2a  11722  fprodm1  11744  fprodp1  11746  fprodunsn  11750  fprodfac  11761  fprodeq0  11763  fprodconst  11766  fprodrec  11775  fproddivap  11776  fprodsplitsn  11779  ege2le3  11817  efaddlem  11820  efsub  11827  efexp  11828  eftlub  11836  efsep  11837  effsumlt  11838  ef4p  11840  tanval3ap  11860  resinval  11861  recosval  11862  efi4p  11863  efival  11878  efmival  11879  efeul  11880  sinadd  11882  cosadd  11883  tanaddap  11885  sinsub  11886  cossub  11887  sincossq  11894  sin2t  11895  cos2t  11896  cos2tsin  11897  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos12dec  11914  absef  11916  absefib  11917  efieq1re  11918  demoivreALT  11920  eirraplem  11923  dvdsexp  12006  oexpneg  12021  opeo  12041  omeo  12042  m1exp1  12045  flodddiv4  12078  flodddiv4t2lthalf  12081  divgcdnnr  12116  gcdaddm  12124  gcdadd  12125  gcdid  12126  modgcd  12131  gcdmultipled  12133  dvdsgcdidd  12134  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  bezoutlemex  12141  bezoutlembz  12144  absmulgcd  12157  gcdmultiple  12160  gcdmultiplez  12161  rpmulgcd  12166  rplpwr  12167  eucalginv  12197  eucalg  12200  lcmneg  12215  lcmgcdlem  12218  lcmgcd  12219  lcmid  12221  lcm1  12222  mulgcddvds  12235  qredeq  12237  divgcdcoprmex  12243  prmind2  12261  rpexp1i  12295  pw2dvdslemn  12306  pw2dvdseulemle  12308  pw2dvdseu  12309  oddpwdclemxy  12310  oddpwdclemdvds  12311  oddpwdclemndvds  12312  oddpwdclemdc  12314  2sqpwodd  12317  nn0gcdsq  12341  phiprmpw  12363  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  fermltl  12375  prmdiv  12376  hashgcdlem  12379  odzdvds  12386  vfermltl  12392  modprm0  12395  nnnn0modprm0  12396  modprmn0modprm0  12397  coprimeprodsq  12398  pythagtriplem1  12406  pythagtriplem4  12409  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  pythagtriplem18  12422  pythagtrip  12424  pcpremul  12434  pceu  12436  pczpre  12438  pcdiv  12443  pcqmul  12444  pcqdiv  12448  pcexp  12450  pcxqcl  12453  pczdvds  12455  pczndvds  12457  pczndvds2  12459  pcid  12465  pcneg  12466  pcdvdstr  12468  pcgcd1  12469  pcgcd  12470  pc2dvds  12471  pcaddlem  12480  pcadd  12481  pcadd2  12482  pcmpt  12484  pcmpt2  12485  fldivp1  12489  pcfac  12491  pcbc  12492  expnprm  12494  prmpwdvds  12496  pockthlem  12497  pockthi  12499  4sqlem7  12525  4sqlem9  12527  4sqlem10  12528  4sqlem2  12530  4sqlem3  12531  4sqlem4  12533  mul4sqlem  12534  4sqlem11  12542  4sqlem16  12547  4sqlem17  12548  4sqlem19  12550  setscomd  12662  ressvalsets  12685  strressid  12692  ressval3d  12693  ressinbasd  12695  ressressg  12696  ressabsg  12697  grpinvalem  12971  grpinva  12972  grprida  12973  isnsgrp  12992  sgrpass  12994  sgrp1  12997  sgrppropd  12999  mnd32g  13011  mnd4g  13013  mndpropd  13024  mhmex  13037  mhmlin  13042  gsumwmhm  13073  grprcan  13112  grpsubval  13121  grpinvid2  13128  grpasscan2  13139  grpsubinv  13148  grpinvadd  13153  grpsubid1  13160  grpsubadd0sub  13162  grpsubadd  13163  grpsubsub  13164  grpaddsubass  13165  grppncan  13166  grpnnncan2  13172  grpsubpropd2  13180  imasgrp2  13183  mhmlem  13187  mhmid  13188  mhmmnd  13189  ghmgrp  13191  mulgnn0gsum  13201  mulgnnp1  13203  mulgaddcomlem  13218  mulgaddcom  13219  mulginvinv  13221  mulgnn0dir  13225  mulgdirlem  13226  mulgp1  13228  mulgneg2  13229  mulgnn0ass  13231  mulgass  13232  mulgmodid  13234  mulgsubdir  13235  nmzsubg  13283  0nsg  13287  eqger  13297  qussub  13310  ghmlin  13321  ghmsub  13324  conjghm  13349  ablsub4  13386  abladdsub4  13387  ablsubsub4  13392  ablsub32  13395  ablnnncan  13396  gsumfzmptfidmadd2  13413  gsumfzconst  13414  gsumfzmhm2  13417  gsumfzsnfd  13418  mgpress  13430  rngass  13438  rngdi  13439  rngdir  13440  rngrz  13445  rngmneg2  13447  rngsubdi  13450  rngsubdir  13451  rngpropd  13454  imasrng  13455  srgass  13470  srgpcomp  13489  srgpcompp  13490  srgpcomppsc  13491  srg1expzeq1  13494  ringpropd  13537  ringrz  13543  ringnegr  13551  ringmneg2  13553  ringsubdi  13555  ringsubdir  13556  ring1  13558  imasring  13563  opprrng  13576  opprring  13578  mulgass3  13584  dvdsrd  13593  unitgrp  13615  invrfvald  13621  dvr1  13637  dvrass  13638  dvrcan1  13639  dvrcan3  13640  rdivmuldivd  13643  subrginv  13736  subrgdv  13737  resrhm2b  13748  islmod  13790  lmodlema  13791  islmodd  13792  lmodvs0  13821  lmodvneg1  13829  lmodvsubval2  13841  lmodsubvs  13842  lmodsubdi  13843  lmodsubdir  13844  lmodprop2d  13847  rmodislmodlem  13849  rmodislmod  13850  lsssn0  13869  sraval  13936  cnfldsub  14074  gsumfzfsumlem0  14085  gsumfzfsumlemm  14086  mulgrhm  14108  mulgrhm2  14109  znval  14135  znval2  14137  znunit  14158  psrval  14163  restabs  14354  cnprcl2k  14385  cnrest2r  14416  ispsmet  14502  psmettri2  14507  psmetsym  14508  ismet  14523  isxmet  14524  xmettri2  14540  xmetsym  14547  xmettri3  14553  mettri3  14554  xblss2ps  14583  xblss2  14584  comet  14678  xmetxp  14686  xmetxpbl  14687  txmetcnp  14697  fsumcncntop  14746  cncfi  14757  divcncfap  14793  limccl  14838  ellimc3apf  14839  limccnpcntop  14854  limccnp2lem  14855  reldvg  14858  dvfvalap  14860  eldvap  14861  dvcj  14888  dvfre  14889  dvexp  14890  dvexp2  14891  dvrecap  14892  dvmptaddx  14898  dvmptmulx  14899  dvmptnegcn  14901  dvmptsubcn  14902  dvmptcjx  14903  dvmptfsum  14904  dveflem  14905  dvef  14906  plyconst  14924  plyaddlem1  14926  plymullem1  14927  plyadd  14930  plymul  14931  plycolemc  14936  plyco  14937  plycjlemc  14938  plycj  14939  plyrecj  14941  dvply1  14943  sin0pilem1  14957  sin0pilem2  14958  efper  14983  sinperlem  14984  efimpi  14995  ptolemy  15000  tangtx  15014  abssinper  15022  cosq34lt1  15026  rpcxpef  15070  rpcxpp1  15082  rpcxpneg  15083  rpcxpsub  15084  rpmulcxp  15085  rpdivcxp  15087  cxpmul  15088  rpcxproot  15089  cxpcom  15112  rpabscxpbnd  15114  rplogbval  15118  rplogbreexp  15126  rplogbzexp  15127  rprelogbmulexp  15129  rprelogbdiv  15130  relogbexpap  15131  rplogbcxp  15136  rpcxplogb  15137  logbgcd1irr  15140  logbgcd1irraplemap  15142  binom4  15152  wilthlem1  15153  lgslem1  15157  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsval4  15177  lgsneg  15181  lgsneg1  15182  lgsmod  15183  lgsdir2  15190  lgsdirprm  15191  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgssq2  15198  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  gausslemma2dlem5  15223  gausslemma2dlem6  15224  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  lgsquad2lem2  15239  lgsquad2  15240  lgsquad3  15241  m1lgs  15242  2lgslem3c  15252  2lgslem3d  15253  2lgslem3d1  15257  2sqlem2  15272  2sqlem3  15274  2sqlem4  15275  2sqlem8  15280  2sqlem9  15281  2sqlem10  15282  qdencn  15587  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trilpo  15603  apdifflemf  15606  apdiff  15608  iswomni0  15611  redcwlpolemeq1  15614  redcwlpo  15615  nconstwlpolem0  15623  nconstwlpolemgt0  15624  nconstwlpo  15626  neapmkv  15628