Theorem oveq2d 5869

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

Syntax hints:   → wi 4   = wceq 1348  (class class class)co 5853

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  csbov1g  5893  caovassg  6011  caovdig  6027  caovdirg  6030  caov32d  6033  caov4d  6037  caov42d  6039  nnaass  6464  nndi  6465  nnmass  6466  nnmsucr  6467  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  addasspig  7292  mulasspig  7294  distrpig  7295  dfplpq2  7316  mulpipq2  7333  addassnqg  7344  prarloclemarch  7380  prarloclemarch2  7381  ltrnqg  7382  enq0sym  7394  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  nq0a0  7419  distrnq0  7421  addassnq0  7424  prarloclemlo  7456  prarloclem3  7459  prarloclem5  7462  prarloclemcalc  7464  addnqprl  7491  addnqpru  7492  prmuloclemcalc  7527  mulnqprl  7530  mulnqpru  7531  distrlem4prl  7546  distrlem4pru  7547  1idprl  7552  1idpru  7553  ltexprlemloc  7569  addcanprleml  7576  addcanprlemu  7577  recexprlem1ssu  7596  ltmprr  7604  caucvgprlemcanl  7606  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlemlim  7623  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexb  7669  caucvgprprlemaddq  7670  caucvgprprlem1  7671  addcmpblnr  7701  mulcmpblnrlemg  7702  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  ltsrprg  7709  recexgt0sr  7735  mulgt0sr  7740  caucvgsrlemgt1  7757  caucvgsrlemoffval  7758  caucvgsr  7764  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  suplocsr  7771  mulcnsr  7797  pitoregt0  7811  recidpirqlemcalc  7819  axmulcom  7833  axmulass  7835  axdistr  7836  ax0id  7840  axcnre  7843  recriota  7852  axcaucvglemcau  7860  axcaucvglemres  7861  mulid1  7917  adddirp1d  7946  mul32  8049  mul31  8050  add32  8078  add4  8080  add42  8081  cnegex  8097  addcan2  8100  addsubass  8129  subsub2  8147  nppcan2  8150  sub32  8153  nnncan  8154  sub4  8164  muladd  8303  subdi  8304  mul2neg  8317  submul2  8318  mulsub  8320  mulsubfacd  8337  add20  8393  recexre  8497  rereim  8505  apreap  8506  ltmul1  8511  cru  8521  apreim  8522  mulreim  8523  apadd1  8527  apneg  8530  mulap0  8572  divrecap  8605  divassap  8607  divmulasscomap  8613  divsubdirap  8625  divdivdivap  8630  divmul24ap  8633  divmuleqap  8634  divcanap6  8636  divdivap1  8640  divdivap2  8641  divsubdivap  8645  conjmulap  8646  div2negap  8652  apmul1  8705  cju  8877  nnmulcl  8899  add1p1  9127  sub1m1  9128  cnm2m1cnm3  9129  xp1d2m1eqxm1d2  9130  div4p1lem1div2  9131  un0addcl  9168  un0mulcl  9169  zaddcllemneg  9251  qapne  9598  cnref1o  9609  rexsub  9810  xnegid  9816  xaddcom  9818  xnegdi  9825  xaddass  9826  xaddass2  9827  xpncan  9828  xnpcan  9829  xleadd1a  9830  xsubge0  9838  xposdif  9839  xlesubadd  9840  xadd4d  9842  lincmb01cmp  9960  iccf1o  9961  ige3m2fz  10005  fztp  10034  fzsuc2  10035  fseq1m1p1  10051  fzm1  10056  ige2m1fz1  10065  nn0split  10092  nnsplit  10093  fzval3  10160  zpnn0elfzo1  10164  fzosplitsnm1  10165  fzosplitprm1  10190  fzoshftral  10194  rebtwn2zlemstep  10209  flhalf  10258  modqval  10280  modqvalr  10281  modqdiffl  10291  modqfrac  10293  flqmod  10294  intqfrac  10295  zmod10  10296  modqmulnn  10298  modqvalp1  10299  modqid  10305  modqcyc  10315  modqcyc2  10316  modqmul1  10333  q2submod  10341  modqdi  10348  modqsubdir  10349  modqeqmodmin  10350  modsumfzodifsn  10352  addmodlteq  10354  frecuzrdgsuctlem  10379  uzsinds  10398  seqeq3  10406  iseqvalcbv  10413  seq3val  10414  seqvalcd  10415  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  seq3m1  10424  seq3fveq2  10425  seq3shft2  10429  monoord2  10433  ser3mono  10434  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  seq3caopr  10439  seq3id2  10465  seq3homo  10466  seq3z  10467  exp3vallem  10477  exp3val  10478  expp1  10483  expnegap0  10484  expineg2  10485  expn1ap0  10486  expm1t  10504  1exp  10505  expnegzap  10510  mulexpzap  10516  expadd  10518  expaddzaplem  10519  expaddzap  10520  expmul  10521  expmulzap  10522  m1expeven  10523  expsubap  10524  expp1zap  10525  expm1ap  10526  expdivap  10527  iexpcyc  10580  subsq2  10583  binom2  10587  binom21  10588  binom2sub  10589  binom2sub1  10590  mulbinom2  10592  binom3  10593  zesq  10594  bernneq  10596  sqoddm1div8  10629  nn0opthlem1d  10654  nn0opthd  10656  facp1  10664  facnn2  10668  faclbnd  10675  faclbnd6  10678  bcval  10683  bccmpl  10688  bcn0  10689  bcnn  10691  bcnp1n  10693  bcm1k  10694  bcp1n  10695  bcp1nk  10696  bcval5  10697  bcp1m1  10699  bcpasc  10700  bcn2m1  10703  bcn2p1  10704  omgadd  10737  hashunlem  10739  hashunsng  10742  hashdifsn  10754  hashxp  10761  zfz1isolemsplit  10773  zfz1isolem1  10775  zfz1iso  10776  seq3coll  10777  shftcan1  10798  shftcan2  10799  cjval  10809  cjth  10810  crre  10821  replim  10823  remim  10824  reim0b  10826  rereb  10827  mulreap  10828  cjreb  10830  recj  10831  reneg  10832  readd  10833  resub  10834  remullem  10835  imcj  10839  imneg  10840  imadd  10841  imsub  10842  cjcj  10847  cjadd  10848  ipcnval  10850  cjmulrcl  10851  cjneg  10854  addcj  10855  cjsub  10856  cnrecnv  10874  caucvgrelemcau  10944  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniqlem  10958  resqrexlemover  10974  resqrexlemlo  10977  resqrexlemcalc1  10978  resqrexlemcalc3  10980  resqrexlemnm  10982  resqrexlemcvg  10983  absneg  11014  abscj  11016  sqabsadd  11019  sqabssub  11020  absmul  11033  absid  11035  absre  11041  absresq  11042  absexpzap  11044  recvalap  11061  abstri  11068  abs2dif2  11071  recan  11073  cau3lem  11078  amgm2  11082  bdtrilem  11202  xrmaxadd  11224  xrbdtri  11239  climaddc1  11292  climsubc1  11295  climcvg1nlem  11312  serf0  11315  summodclem3  11343  summodclem2a  11344  summodc  11346  fsumsplitsn  11373  fsumm1  11379  fsumsplitsnun  11382  fsump1  11383  isummulc2  11389  fsumrev  11406  fisum0diag2  11410  fsummulc2  11411  fsumsub  11415  fsumabs  11428  telfsumo  11429  fsumparts  11433  fsumrelem  11434  fsumiun  11440  binomlem  11446  binom  11447  binom1p  11448  binom11  11449  binom1dif  11450  bcxmas  11452  isumsplit  11454  isum1p  11455  divcnv  11460  arisum2  11462  trireciplem  11463  trirecip  11464  geolim  11474  georeclim  11476  geo2sum  11477  geo2lim  11479  geoisum1c  11483  0.999...  11484  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratz  11495  mertenslem2  11499  mertensabs  11500  clim2prod  11502  prodfrecap  11509  prodfdivap  11510  prodmodclem3  11538  prodmodclem2a  11539  fprodm1  11561  fprodp1  11563  fprodunsn  11567  fprodfac  11578  fprodeq0  11580  fprodconst  11583  fprodrec  11592  fproddivap  11593  fprodsplitsn  11596  ege2le3  11634  efaddlem  11637  efsub  11644  efexp  11645  eftlub  11653  efsep  11654  effsumlt  11655  ef4p  11657  tanval3ap  11677  resinval  11678  recosval  11679  efi4p  11680  efival  11695  efmival  11696  efeul  11697  sinadd  11699  cosadd  11700  tanaddap  11702  sinsub  11703  cossub  11704  sincossq  11711  sin2t  11712  cos2t  11713  cos2tsin  11714  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  cos12dec  11730  absef  11732  absefib  11733  efieq1re  11734  demoivreALT  11736  eirraplem  11739  dvdsexp  11821  oexpneg  11836  opeo  11856  omeo  11857  m1exp1  11860  flodddiv4  11893  flodddiv4t2lthalf  11896  divgcdnnr  11931  gcdaddm  11939  gcdadd  11940  gcdid  11941  modgcd  11946  gcdmultipled  11948  dvdsgcdidd  11949  bezoutlemnewy  11951  bezoutlema  11954  bezoutlemb  11955  bezoutlemex  11956  bezoutlembz  11959  absmulgcd  11972  gcdmultiple  11975  gcdmultiplez  11976  rpmulgcd  11981  rplpwr  11982  eucalginv  12010  eucalg  12013  lcmneg  12028  lcmgcdlem  12031  lcmgcd  12032  lcmid  12034  lcm1  12035  mulgcddvds  12048  qredeq  12050  divgcdcoprmex  12056  prmind2  12074  rpexp1i  12108  pw2dvdslemn  12119  pw2dvdseulemle  12121  pw2dvdseu  12122  oddpwdclemxy  12123  oddpwdclemdvds  12124  oddpwdclemndvds  12125  oddpwdclemdc  12127  2sqpwodd  12130  nn0gcdsq  12154  phiprmpw  12176  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  fermltl  12188  prmdiv  12189  hashgcdlem  12192  odzdvds  12199  vfermltl  12205  modprm0  12208  nnnn0modprm0  12209  modprmn0modprm0  12210  coprimeprodsq  12211  pythagtriplem1  12219  pythagtriplem4  12222  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem16  12233  pythagtriplem18  12235  pythagtrip  12237  pcpremul  12247  pceu  12249  pczpre  12251  pcdiv  12256  pcqmul  12257  pcqdiv  12261  pcexp  12263  pczdvds  12267  pczndvds  12269  pczndvds2  12271  pcid  12277  pcneg  12278  pcdvdstr  12280  pcgcd1  12281  pcgcd  12282  pc2dvds  12283  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcmpt2  12296  fldivp1  12300  pcfac  12302  pcbc  12303  expnprm  12305  prmpwdvds  12307  pockthlem  12308  pockthi  12310  4sqlem7  12336  4sqlem9  12338  4sqlem10  12339  4sqlem2  12341  4sqlem3  12342  4sqlem4  12344  mul4sqlem  12345  grprinvlem  12639  grprinvd  12640  grpridd  12641  isnsgrp  12647  sgrpass  12649  sgrp1  12651  mnd32g  12663  mnd4g  12665  mndpropd  12676  mhmlin  12690  grprcan  12740  grpsubval  12749  grpinvid2  12755  grpasscan2  12763  grpsubinv  12772  restabs  12969  cnprcl2k  13000  cnrest2r  13031  ispsmet  13117  psmettri2  13122  psmetsym  13123  ismet  13138  isxmet  13139  xmettri2  13155  xmetsym  13162  xmettri3  13168  mettri3  13169  xblss2ps  13198  xblss2  13199  comet  13293  xmetxp  13301  xmetxpbl  13302  txmetcnp  13312  fsumcncntop  13350  cncfi  13359  limccl  13422  ellimc3apf  13423  limccnpcntop  13438  limccnp2lem  13439  reldvg  13442  dvfvalap  13444  eldvap  13445  dvcj  13467  dvfre  13468  dvexp  13469  dvexp2  13470  dvrecap  13471  dvmptaddx  13475  dvmptmulx  13476  dvmptnegcn  13478  dvmptsubcn  13479  dvmptcjx  13480  dveflem  13481  dvef  13482  sin0pilem1  13496  sin0pilem2  13497  efper  13522  sinperlem  13523  efimpi  13534  ptolemy  13539  tangtx  13553  abssinper  13561  cosq34lt1  13565  rpcxpef  13609  rpcxpp1  13621  rpcxpneg  13622  rpcxpsub  13623  rpmulcxp  13624  rpdivcxp  13626  cxpmul  13627  rpcxproot  13628  cxpcom  13651  rpabscxpbnd  13653  rplogbval  13657  rplogbreexp  13665  rplogbzexp  13666  rprelogbmulexp  13668  rprelogbdiv  13669  relogbexpap  13670  rplogbcxp  13675  rpcxplogb  13676  logbgcd1irr  13679  logbgcd1irraplemap  13681  binom4  13691  lgslem1  13695  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsval4  13715  lgsneg  13719  lgsneg1  13720  lgsmod  13721  lgsdir2  13728  lgsdirprm  13729  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgssq2  13736  lgsdirnn0  13742  lgsdinn0  13743  2sqlem2  13745  2sqlem3  13747  2sqlem4  13748  2sqlem8  13753  2sqlem9  13754  2sqlem10  13755  qdencn  14059  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trilpo  14075  apdifflemf  14078  apdiff  14080  iswomni0  14083  redcwlpolemeq1  14086  redcwlpo  14087  nconstwlpolem0  14094  nconstwlpolemgt0  14095  nconstwlpo  14097  neapmkv  14099