Theorem oveq2d 5798

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

Syntax hints:   → wi 4   = wceq 1332  (class class class)co 5782

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  csbov1g  5819  caovassg  5937  caovdig  5953  caovdirg  5956  caov32d  5959  caov4d  5963  caov42d  5965  grprinvlem  5973  grprinvd  5974  grpridd  5975  nnaass  6389  nndi  6390  nnmass  6391  nnmsucr  6392  ecovass  6546  ecoviass  6547  ecovdi  6548  ecovidi  6549  addasspig  7162  mulasspig  7164  distrpig  7165  dfplpq2  7186  mulpipq2  7203  addassnqg  7214  prarloclemarch  7250  prarloclemarch2  7251  ltrnqg  7252  enq0sym  7264  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  nq0a0  7289  distrnq0  7291  addassnq0  7294  prarloclemlo  7326  prarloclem3  7329  prarloclem5  7332  prarloclemcalc  7334  addnqprl  7361  addnqpru  7362  prmuloclemcalc  7397  mulnqprl  7400  mulnqpru  7401  distrlem4prl  7416  distrlem4pru  7417  1idprl  7422  1idpru  7423  ltexprlemloc  7439  addcanprleml  7446  addcanprlemu  7447  recexprlem1ssu  7466  ltmprr  7474  caucvgprlemcanl  7476  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlemlim  7493  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnkeqj  7522  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexb  7539  caucvgprprlemaddq  7540  caucvgprprlem1  7541  addcmpblnr  7571  mulcmpblnrlemg  7572  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  ltsrprg  7579  recexgt0sr  7605  mulgt0sr  7610  caucvgsrlemgt1  7627  caucvgsrlemoffval  7628  caucvgsr  7634  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  suplocsr  7641  mulcnsr  7667  pitoregt0  7681  recidpirqlemcalc  7689  axmulcom  7703  axmulass  7705  axdistr  7706  ax0id  7710  axcnre  7713  recriota  7722  axcaucvglemcau  7730  axcaucvglemres  7731  mulid1  7787  adddirp1d  7816  mul32  7916  mul31  7917  add32  7945  add4  7947  add42  7948  cnegex  7964  addcan2  7967  addsubass  7996  subsub2  8014  nppcan2  8017  sub32  8020  nnncan  8021  sub4  8031  muladd  8170  subdi  8171  mul2neg  8184  submul2  8185  mulsub  8187  mulsubfacd  8204  add20  8260  recexre  8364  rereim  8372  apreap  8373  ltmul1  8378  cru  8388  apreim  8389  mulreim  8390  apadd1  8394  apneg  8397  mulap0  8439  divrecap  8472  divassap  8474  divmulasscomap  8480  divsubdirap  8492  divdivdivap  8497  divmul24ap  8500  divmuleqap  8501  divcanap6  8503  divdivap1  8507  divdivap2  8508  divsubdivap  8512  conjmulap  8513  div2negap  8519  apmul1  8572  cju  8743  nnmulcl  8765  add1p1  8993  sub1m1  8994  cnm2m1cnm3  8995  xp1d2m1eqxm1d2  8996  div4p1lem1div2  8997  un0addcl  9034  un0mulcl  9035  zaddcllemneg  9117  qapne  9458  cnref1o  9469  rexsub  9666  xnegid  9672  xaddcom  9674  xnegdi  9681  xaddass  9682  xaddass2  9683  xpncan  9684  xnpcan  9685  xleadd1a  9686  xsubge0  9694  xposdif  9695  xlesubadd  9696  xadd4d  9698  lincmb01cmp  9816  iccf1o  9817  ige3m2fz  9860  fztp  9889  fzsuc2  9890  fseq1m1p1  9906  fzm1  9911  ige2m1fz1  9920  nn0split  9944  nnsplit  9945  fzval3  10012  zpnn0elfzo1  10016  fzosplitsnm1  10017  fzosplitprm1  10042  fzoshftral  10046  rebtwn2zlemstep  10061  flhalf  10106  modqval  10128  modqvalr  10129  modqdiffl  10139  modqfrac  10141  flqmod  10142  intqfrac  10143  zmod10  10144  modqmulnn  10146  modqvalp1  10147  modqid  10153  modqcyc  10163  modqcyc2  10164  modqmul1  10181  q2submod  10189  modqdi  10196  modqsubdir  10197  modqeqmodmin  10198  modsumfzodifsn  10200  addmodlteq  10202  frecuzrdgsuctlem  10227  uzsinds  10246  seqeq3  10254  iseqvalcbv  10261  seq3val  10262  seqvalcd  10263  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  seq3m1  10272  seq3fveq2  10273  seq3shft2  10277  monoord2  10281  ser3mono  10282  seq3split  10283  seq3caopr3  10285  seq3caopr2  10286  seq3caopr  10287  seq3id2  10313  seq3homo  10314  seq3z  10315  exp3vallem  10325  exp3val  10326  expp1  10331  expnegap0  10332  expineg2  10333  expn1ap0  10334  expm1t  10352  1exp  10353  expnegzap  10358  mulexpzap  10364  expadd  10366  expaddzaplem  10367  expaddzap  10368  expmul  10369  expmulzap  10370  m1expeven  10371  expsubap  10372  expp1zap  10373  expm1ap  10374  expdivap  10375  iexpcyc  10428  subsq2  10431  binom2  10434  binom21  10435  binom2sub  10436  binom2sub1  10437  mulbinom2  10439  binom3  10440  zesq  10441  bernneq  10443  sqoddm1div8  10475  nn0opthlem1d  10498  nn0opthd  10500  facp1  10508  facnn2  10512  faclbnd  10519  faclbnd6  10522  bcval  10527  bccmpl  10532  bcn0  10533  bcnn  10535  bcnp1n  10537  bcm1k  10538  bcp1n  10539  bcp1nk  10540  bcval5  10541  bcp1m1  10543  bcpasc  10544  bcn2m1  10547  bcn2p1  10548  omgadd  10580  hashunlem  10582  hashunsng  10585  hashdifsn  10597  hashxp  10604  zfz1isolemsplit  10613  zfz1isolem1  10615  zfz1iso  10616  seq3coll  10617  shftcan1  10638  shftcan2  10639  cjval  10649  cjth  10650  crre  10661  replim  10663  remim  10664  reim0b  10666  rereb  10667  mulreap  10668  cjreb  10670  recj  10671  reneg  10672  readd  10673  resub  10674  remullem  10675  imcj  10679  imneg  10680  imadd  10681  imsub  10682  cjcj  10687  cjadd  10688  ipcnval  10690  cjmulrcl  10691  cjneg  10694  addcj  10695  cjsub  10696  cnrecnv  10714  caucvgrelemcau  10784  cvg1nlemcau  10788  cvg1nlemres  10789  recvguniqlem  10798  resqrexlemover  10814  resqrexlemlo  10817  resqrexlemcalc1  10818  resqrexlemcalc3  10820  resqrexlemnm  10822  resqrexlemcvg  10823  absneg  10854  abscj  10856  sqabsadd  10859  sqabssub  10860  absmul  10873  absid  10875  absre  10881  absresq  10882  absexpzap  10884  recvalap  10901  abstri  10908  abs2dif2  10911  recan  10913  cau3lem  10918  amgm2  10922  bdtrilem  11042  xrmaxadd  11062  xrbdtri  11077  climaddc1  11130  climsubc1  11133  climcvg1nlem  11150  serf0  11153  summodclem3  11181  summodclem2a  11182  summodc  11184  fsumsplitsn  11211  fsumm1  11217  fsumsplitsnun  11220  fsump1  11221  isummulc2  11227  fsumrev  11244  fisum0diag2  11248  fsummulc2  11249  fsumsub  11253  fsumabs  11266  telfsumo  11267  fsumparts  11271  fsumrelem  11272  fsumiun  11278  binomlem  11284  binom  11285  binom1p  11286  binom11  11287  binom1dif  11288  bcxmas  11290  isumsplit  11292  isum1p  11293  divcnv  11298  arisum2  11300  trireciplem  11301  trirecip  11302  geolim  11312  georeclim  11314  geo2sum  11315  geo2lim  11317  geoisum1c  11321  0.999...  11322  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratz  11333  mertenslem2  11337  mertensabs  11338  clim2prod  11340  prodfrecap  11347  prodfdivap  11348  prodmodclem3  11376  prodmodclem2a  11377  ege2le3  11414  efaddlem  11417  efsub  11424  efexp  11425  eftlub  11433  efsep  11434  effsumlt  11435  ef4p  11437  tanval3ap  11457  resinval  11458  recosval  11459  efi4p  11460  efival  11475  efmival  11476  efeul  11477  sinadd  11479  cosadd  11480  tanaddap  11482  sinsub  11483  cossub  11484  sincossq  11491  sin2t  11492  cos2t  11493  cos2tsin  11494  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  cos12dec  11510  absef  11512  absefib  11513  efieq1re  11514  demoivreALT  11516  eirraplem  11519  dvdsexp  11595  oexpneg  11610  opeo  11630  omeo  11631  m1exp1  11634  flodddiv4  11667  flodddiv4t2lthalf  11670  divgcdnnr  11700  gcdaddm  11708  gcdadd  11709  gcdid  11710  modgcd  11715  gcdmultipled  11717  dvdsgcdidd  11718  bezoutlemnewy  11720  bezoutlema  11723  bezoutlemb  11724  bezoutlemex  11725  bezoutlembz  11728  absmulgcd  11741  gcdmultiple  11744  gcdmultiplez  11745  rpmulgcd  11750  rplpwr  11751  eucalginv  11773  eucalg  11776  lcmneg  11791  lcmgcdlem  11794  lcmgcd  11795  lcmid  11797  lcm1  11798  mulgcddvds  11811  qredeq  11813  divgcdcoprmex  11819  prmind2  11837  rpexp1i  11868  pw2dvdslemn  11879  pw2dvdseulemle  11881  pw2dvdseu  11882  oddpwdclemxy  11883  oddpwdclemdvds  11884  oddpwdclemndvds  11885  oddpwdclemdc  11887  2sqpwodd  11890  nn0gcdsq  11914  phiprmpw  11934  hashgcdlem  11939  restabs  12383  cnprcl2k  12414  cnrest2r  12445  ispsmet  12531  psmettri2  12536  psmetsym  12537  ismet  12552  isxmet  12553  xmettri2  12569  xmetsym  12576  xmettri3  12582  mettri3  12583  xblss2ps  12612  xblss2  12613  comet  12707  xmetxp  12715  xmetxpbl  12716  txmetcnp  12726  fsumcncntop  12764  cncfi  12773  limccl  12836  ellimc3apf  12837  limccnpcntop  12852  limccnp2lem  12853  reldvg  12856  dvfvalap  12858  eldvap  12859  dvcj  12881  dvfre  12882  dvexp  12883  dvexp2  12884  dvrecap  12885  dvmptaddx  12889  dvmptmulx  12890  dvmptnegcn  12892  dvmptsubcn  12893  dvmptcjx  12894  dveflem  12895  dvef  12896  sin0pilem1  12910  sin0pilem2  12911  efper  12936  sinperlem  12937  efimpi  12948  ptolemy  12953  tangtx  12967  abssinper  12975  cosq34lt1  12979  rpcxpef  13023  rpcxpp1  13035  rpcxpneg  13036  rpcxpsub  13037  rpmulcxp  13038  rpdivcxp  13040  cxpmul  13041  rpcxproot  13042  cxpcom  13065  rpabscxpbnd  13067  rplogbval  13070  rplogbreexp  13078  rplogbzexp  13079  rprelogbmulexp  13081  rprelogbdiv  13082  relogbexpap  13083  rplogbcxp  13088  rpcxplogb  13089  logbgcd1irr  13092  logbgcd1irraplemap  13094  qdencn  13397  trilpolemclim  13404  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trilpo  13411  apdifflemf  13414  apdiff  13416  redcwlpolemeq1  13421  redcwlpo  13422  neapmkv  13425