Theorem oveq2d 5857

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

Syntax hints:   → wi 4   = wceq 1343  (class class class)co 5841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  csbov1g  5878  caovassg  5996  caovdig  6012  caovdirg  6015  caov32d  6018  caov4d  6022  caov42d  6024  grprinvlem  6032  grprinvd  6033  grpridd  6034  nnaass  6449  nndi  6450  nnmass  6451  nnmsucr  6452  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  addasspig  7267  mulasspig  7269  distrpig  7270  dfplpq2  7291  mulpipq2  7308  addassnqg  7319  prarloclemarch  7355  prarloclemarch2  7356  ltrnqg  7357  enq0sym  7369  addnq0mo  7384  mulnq0mo  7385  addnnnq0  7386  nq0a0  7394  distrnq0  7396  addassnq0  7399  prarloclemlo  7431  prarloclem3  7434  prarloclem5  7437  prarloclemcalc  7439  addnqprl  7466  addnqpru  7467  prmuloclemcalc  7502  mulnqprl  7505  mulnqpru  7506  distrlem4prl  7521  distrlem4pru  7522  1idprl  7527  1idpru  7528  ltexprlemloc  7544  addcanprleml  7551  addcanprlemu  7552  recexprlem1ssu  7571  ltmprr  7579  caucvgprlemcanl  7581  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlemlim  7598  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnkeqj  7627  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemloc  7640  caucvgprprlemclphr  7642  caucvgprprlemexb  7644  caucvgprprlemaddq  7645  caucvgprprlem1  7646  addcmpblnr  7676  mulcmpblnrlemg  7677  addsrmo  7680  mulsrmo  7681  addsrpr  7682  mulsrpr  7683  ltsrprg  7684  recexgt0sr  7710  mulgt0sr  7715  caucvgsrlemgt1  7732  caucvgsrlemoffval  7733  caucvgsr  7739  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  suplocsr  7746  mulcnsr  7772  pitoregt0  7786  recidpirqlemcalc  7794  axmulcom  7808  axmulass  7810  axdistr  7811  ax0id  7815  axcnre  7818  recriota  7827  axcaucvglemcau  7835  axcaucvglemres  7836  mulid1  7892  adddirp1d  7921  mul32  8024  mul31  8025  add32  8053  add4  8055  add42  8056  cnegex  8072  addcan2  8075  addsubass  8104  subsub2  8122  nppcan2  8125  sub32  8128  nnncan  8129  sub4  8139  muladd  8278  subdi  8279  mul2neg  8292  submul2  8293  mulsub  8295  mulsubfacd  8312  add20  8368  recexre  8472  rereim  8480  apreap  8481  ltmul1  8486  cru  8496  apreim  8497  mulreim  8498  apadd1  8502  apneg  8505  mulap0  8547  divrecap  8580  divassap  8582  divmulasscomap  8588  divsubdirap  8600  divdivdivap  8605  divmul24ap  8608  divmuleqap  8609  divcanap6  8611  divdivap1  8615  divdivap2  8616  divsubdivap  8620  conjmulap  8621  div2negap  8627  apmul1  8680  cju  8852  nnmulcl  8874  add1p1  9102  sub1m1  9103  cnm2m1cnm3  9104  xp1d2m1eqxm1d2  9105  div4p1lem1div2  9106  un0addcl  9143  un0mulcl  9144  zaddcllemneg  9226  qapne  9573  cnref1o  9584  rexsub  9785  xnegid  9791  xaddcom  9793  xnegdi  9800  xaddass  9801  xaddass2  9802  xpncan  9803  xnpcan  9804  xleadd1a  9805  xsubge0  9813  xposdif  9814  xlesubadd  9815  xadd4d  9817  lincmb01cmp  9935  iccf1o  9936  ige3m2fz  9980  fztp  10009  fzsuc2  10010  fseq1m1p1  10026  fzm1  10031  ige2m1fz1  10040  nn0split  10067  nnsplit  10068  fzval3  10135  zpnn0elfzo1  10139  fzosplitsnm1  10140  fzosplitprm1  10165  fzoshftral  10169  rebtwn2zlemstep  10184  flhalf  10233  modqval  10255  modqvalr  10256  modqdiffl  10266  modqfrac  10268  flqmod  10269  intqfrac  10270  zmod10  10271  modqmulnn  10273  modqvalp1  10274  modqid  10280  modqcyc  10290  modqcyc2  10291  modqmul1  10308  q2submod  10316  modqdi  10323  modqsubdir  10324  modqeqmodmin  10325  modsumfzodifsn  10327  addmodlteq  10329  frecuzrdgsuctlem  10354  uzsinds  10373  seqeq3  10381  iseqvalcbv  10388  seq3val  10389  seqvalcd  10390  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  seq3m1  10399  seq3fveq2  10400  seq3shft2  10404  monoord2  10408  ser3mono  10409  seq3split  10410  seq3caopr3  10412  seq3caopr2  10413  seq3caopr  10414  seq3id2  10440  seq3homo  10441  seq3z  10442  exp3vallem  10452  exp3val  10453  expp1  10458  expnegap0  10459  expineg2  10460  expn1ap0  10461  expm1t  10479  1exp  10480  expnegzap  10485  mulexpzap  10491  expadd  10493  expaddzaplem  10494  expaddzap  10495  expmul  10496  expmulzap  10497  m1expeven  10498  expsubap  10499  expp1zap  10500  expm1ap  10501  expdivap  10502  iexpcyc  10555  subsq2  10558  binom2  10562  binom21  10563  binom2sub  10564  binom2sub1  10565  mulbinom2  10567  binom3  10568  zesq  10569  bernneq  10571  sqoddm1div8  10604  nn0opthlem1d  10629  nn0opthd  10631  facp1  10639  facnn2  10643  faclbnd  10650  faclbnd6  10653  bcval  10658  bccmpl  10663  bcn0  10664  bcnn  10666  bcnp1n  10668  bcm1k  10669  bcp1n  10670  bcp1nk  10671  bcval5  10672  bcp1m1  10674  bcpasc  10675  bcn2m1  10678  bcn2p1  10679  omgadd  10711  hashunlem  10713  hashunsng  10716  hashdifsn  10728  hashxp  10735  zfz1isolemsplit  10747  zfz1isolem1  10749  zfz1iso  10750  seq3coll  10751  shftcan1  10772  shftcan2  10773  cjval  10783  cjth  10784  crre  10795  replim  10797  remim  10798  reim0b  10800  rereb  10801  mulreap  10802  cjreb  10804  recj  10805  reneg  10806  readd  10807  resub  10808  remullem  10809  imcj  10813  imneg  10814  imadd  10815  imsub  10816  cjcj  10821  cjadd  10822  ipcnval  10824  cjmulrcl  10825  cjneg  10828  addcj  10829  cjsub  10830  cnrecnv  10848  caucvgrelemcau  10918  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniqlem  10932  resqrexlemover  10948  resqrexlemlo  10951  resqrexlemcalc1  10952  resqrexlemcalc3  10954  resqrexlemnm  10956  resqrexlemcvg  10957  absneg  10988  abscj  10990  sqabsadd  10993  sqabssub  10994  absmul  11007  absid  11009  absre  11015  absresq  11016  absexpzap  11018  recvalap  11035  abstri  11042  abs2dif2  11045  recan  11047  cau3lem  11052  amgm2  11056  bdtrilem  11176  xrmaxadd  11198  xrbdtri  11213  climaddc1  11266  climsubc1  11269  climcvg1nlem  11286  serf0  11289  summodclem3  11317  summodclem2a  11318  summodc  11320  fsumsplitsn  11347  fsumm1  11353  fsumsplitsnun  11356  fsump1  11357  isummulc2  11363  fsumrev  11380  fisum0diag2  11384  fsummulc2  11385  fsumsub  11389  fsumabs  11402  telfsumo  11403  fsumparts  11407  fsumrelem  11408  fsumiun  11414  binomlem  11420  binom  11421  binom1p  11422  binom11  11423  binom1dif  11424  bcxmas  11426  isumsplit  11428  isum1p  11429  divcnv  11434  arisum2  11436  trireciplem  11437  trirecip  11438  geolim  11448  georeclim  11450  geo2sum  11451  geo2lim  11453  geoisum1c  11457  0.999...  11458  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratz  11469  mertenslem2  11473  mertensabs  11474  clim2prod  11476  prodfrecap  11483  prodfdivap  11484  prodmodclem3  11512  prodmodclem2a  11513  fprodm1  11535  fprodp1  11537  fprodunsn  11541  fprodfac  11552  fprodeq0  11554  fprodconst  11557  fprodrec  11566  fproddivap  11567  fprodsplitsn  11570  ege2le3  11608  efaddlem  11611  efsub  11618  efexp  11619  eftlub  11627  efsep  11628  effsumlt  11629  ef4p  11631  tanval3ap  11651  resinval  11652  recosval  11653  efi4p  11654  efival  11669  efmival  11670  efeul  11671  sinadd  11673  cosadd  11674  tanaddap  11676  sinsub  11677  cossub  11678  sincossq  11685  sin2t  11686  cos2t  11687  cos2tsin  11688  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  cos12dec  11704  absef  11706  absefib  11707  efieq1re  11708  demoivreALT  11710  eirraplem  11713  dvdsexp  11795  oexpneg  11810  opeo  11830  omeo  11831  m1exp1  11834  flodddiv4  11867  flodddiv4t2lthalf  11870  divgcdnnr  11905  gcdaddm  11913  gcdadd  11914  gcdid  11915  modgcd  11920  gcdmultipled  11922  dvdsgcdidd  11923  bezoutlemnewy  11925  bezoutlema  11928  bezoutlemb  11929  bezoutlemex  11930  bezoutlembz  11933  absmulgcd  11946  gcdmultiple  11949  gcdmultiplez  11950  rpmulgcd  11955  rplpwr  11956  eucalginv  11984  eucalg  11987  lcmneg  12002  lcmgcdlem  12005  lcmgcd  12006  lcmid  12008  lcm1  12009  mulgcddvds  12022  qredeq  12024  divgcdcoprmex  12030  prmind2  12048  rpexp1i  12082  pw2dvdslemn  12093  pw2dvdseulemle  12095  pw2dvdseu  12096  oddpwdclemxy  12097  oddpwdclemdvds  12098  oddpwdclemndvds  12099  oddpwdclemdc  12101  2sqpwodd  12104  nn0gcdsq  12128  phiprmpw  12150  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  fermltl  12162  prmdiv  12163  hashgcdlem  12166  odzdvds  12173  vfermltl  12179  modprm0  12182  nnnn0modprm0  12183  modprmn0modprm0  12184  coprimeprodsq  12185  pythagtriplem1  12193  pythagtriplem4  12196  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  pythagtriplem18  12209  pythagtrip  12211  pcpremul  12221  pceu  12223  pczpre  12225  pcdiv  12230  pcqmul  12231  pcqdiv  12235  pcexp  12237  pczdvds  12241  pczndvds  12243  pczndvds2  12245  pcid  12251  pcneg  12252  pcdvdstr  12254  pcgcd1  12255  pcgcd  12256  pc2dvds  12257  pcaddlem  12266  pcadd  12267  pcmpt  12269  pcmpt2  12270  fldivp1  12274  pcfac  12276  pcbc  12277  expnprm  12279  prmpwdvds  12281  pockthlem  12282  pockthi  12284  4sqlem7  12310  4sqlem9  12312  4sqlem10  12313  4sqlem2  12315  4sqlem3  12316  4sqlem4  12318  mul4sqlem  12319  restabs  12775  cnprcl2k  12806  cnrest2r  12837  ispsmet  12923  psmettri2  12928  psmetsym  12929  ismet  12944  isxmet  12945  xmettri2  12961  xmetsym  12968  xmettri3  12974  mettri3  12975  xblss2ps  13004  xblss2  13005  comet  13099  xmetxp  13107  xmetxpbl  13108  txmetcnp  13118  fsumcncntop  13156  cncfi  13165  limccl  13228  ellimc3apf  13229  limccnpcntop  13244  limccnp2lem  13245  reldvg  13248  dvfvalap  13250  eldvap  13251  dvcj  13273  dvfre  13274  dvexp  13275  dvexp2  13276  dvrecap  13277  dvmptaddx  13281  dvmptmulx  13282  dvmptnegcn  13284  dvmptsubcn  13285  dvmptcjx  13286  dveflem  13287  dvef  13288  sin0pilem1  13302  sin0pilem2  13303  efper  13328  sinperlem  13329  efimpi  13340  ptolemy  13345  tangtx  13359  abssinper  13367  cosq34lt1  13371  rpcxpef  13415  rpcxpp1  13427  rpcxpneg  13428  rpcxpsub  13429  rpmulcxp  13430  rpdivcxp  13432  cxpmul  13433  rpcxproot  13434  cxpcom  13457  rpabscxpbnd  13459  rplogbval  13463  rplogbreexp  13471  rplogbzexp  13472  rprelogbmulexp  13474  rprelogbdiv  13475  relogbexpap  13476  rplogbcxp  13481  rpcxplogb  13482  logbgcd1irr  13485  logbgcd1irraplemap  13487  binom4  13497  lgslem1  13501  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsval4  13521  lgsneg  13525  lgsneg1  13526  lgsmod  13527  lgsdir2  13534  lgsdirprm  13535  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgssq2  13542  lgsdirnn0  13548  lgsdinn0  13549  2sqlem2  13551  2sqlem3  13553  2sqlem4  13554  2sqlem8  13559  2sqlem9  13560  2sqlem10  13561  qdencn  13866  trilpolemclim  13875  trilpolemcl  13876  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  trilpo  13882  apdifflemf  13885  apdiff  13887  iswomni0  13890  redcwlpolemeq1  13893  redcwlpo  13894  nconstwlpolem0  13901  nconstwlpolemgt0  13902  nconstwlpo  13904  neapmkv  13906