Theorem oveq2d 5941

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  csbov1g  5966  caovassg  6086  caovdig  6102  caovdirg  6105  caov32d  6108  caov4d  6112  caov42d  6114  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  addasspig  7416  mulasspig  7418  distrpig  7419  dfplpq2  7440  mulpipq2  7457  addassnqg  7468  prarloclemarch  7504  prarloclemarch2  7505  ltrnqg  7506  enq0sym  7518  addnq0mo  7533  mulnq0mo  7534  addnnnq0  7535  nq0a0  7543  distrnq0  7545  addassnq0  7548  prarloclemlo  7580  prarloclem3  7583  prarloclem5  7586  prarloclemcalc  7588  addnqprl  7615  addnqpru  7616  prmuloclemcalc  7651  mulnqprl  7654  mulnqpru  7655  distrlem4prl  7670  distrlem4pru  7671  1idprl  7676  1idpru  7677  ltexprlemloc  7693  addcanprleml  7700  addcanprlemu  7701  recexprlem1ssu  7720  ltmprr  7728  caucvgprlemcanl  7730  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlemlim  7747  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgpr  7768  caucvgprprlemell  7771  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemnkeqj  7776  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemloc  7789  caucvgprprlemclphr  7791  caucvgprprlemexb  7793  caucvgprprlemaddq  7794  caucvgprprlem1  7795  addcmpblnr  7825  mulcmpblnrlemg  7826  addsrmo  7829  mulsrmo  7830  addsrpr  7831  mulsrpr  7832  ltsrprg  7833  recexgt0sr  7859  mulgt0sr  7864  caucvgsrlemgt1  7881  caucvgsrlemoffval  7882  caucvgsr  7888  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  suplocsr  7895  mulcnsr  7921  pitoregt0  7935  recidpirqlemcalc  7943  axmulcom  7957  axmulass  7959  axdistr  7960  ax0id  7964  axcnre  7967  recriota  7976  axcaucvglemcau  7984  axcaucvglemres  7985  mulrid  8042  adddirp1d  8072  mul32  8175  mul31  8176  add32  8204  add4  8206  add42  8207  cnegex  8223  addcan2  8226  addsubass  8255  subsub2  8273  nppcan2  8276  sub32  8279  nnncan  8280  sub4  8290  muladd  8429  subdi  8430  mul2neg  8443  submul2  8444  mulsub  8446  muls1d  8463  mulsubfacd  8464  add20  8520  recexre  8624  rereim  8632  apreap  8633  ltmul1  8638  cru  8648  apreim  8649  mulreim  8650  apadd1  8654  apneg  8657  mulap0  8700  divrecap  8734  divassap  8736  divmulasscomap  8742  divsubdirap  8754  divdivdivap  8759  divmul24ap  8762  divmuleqap  8763  divcanap6  8765  divdivap1  8769  divdivap2  8770  divsubdivap  8774  conjmulap  8775  div2negap  8781  apmul1  8834  cju  9007  nnmulcl  9030  add1p1  9260  sub1m1  9261  cnm2m1cnm3  9262  xp1d2m1eqxm1d2  9263  div4p1lem1div2  9264  un0addcl  9301  un0mulcl  9302  zaddcllemneg  9384  qapne  9732  cnref1o  9744  rexsub  9947  xnegid  9953  xaddcom  9955  xnegdi  9962  xaddass  9963  xaddass2  9964  xpncan  9965  xnpcan  9966  xleadd1a  9967  xsubge0  9975  xposdif  9976  xlesubadd  9977  xadd4d  9979  lincmb01cmp  10097  iccf1o  10098  ige3m2fz  10143  fztp  10172  fzsuc2  10173  fseq1m1p1  10189  fzm1  10194  ige2m1fz1  10203  nn0split  10230  nnsplit  10231  fzval3  10299  zpnn0elfzo1  10303  fzosplitsnm1  10304  fzosplitprm1  10329  fzoshftral  10333  rebtwn2zlemstep  10361  flhalf  10411  fldiv4lem1div2uz2  10415  modqval  10435  modqvalr  10436  modqdiffl  10446  modqfrac  10448  flqmod  10449  intqfrac  10450  zmod10  10451  modqmulnn  10453  modqvalp1  10454  modqid  10460  modqcyc  10470  modqcyc2  10471  modqmul1  10488  q2submod  10496  modqdi  10503  modqsubdir  10504  modqeqmodmin  10505  modsumfzodifsn  10507  addmodlteq  10509  frecuzrdgsuctlem  10534  uzsinds  10555  seqeq3  10563  iseqvalcbv  10570  seq3val  10571  seqvalcd  10572  seqf  10575  seq3p1  10576  seqovcd  10578  seqp1cd  10581  seq3m1  10584  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord2  10597  ser3mono  10598  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seq3caopr2  10604  seqcaopr2g  10605  seq3caopr  10606  seqcaoprg  10607  seqf1oglem2a  10629  seqf1oglem2  10631  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  exp3vallem  10651  exp3val  10652  expp1  10657  expnegap0  10658  expineg2  10659  expn1ap0  10660  expm1t  10678  1exp  10679  expnegzap  10684  mulexpzap  10690  expadd  10692  expaddzaplem  10693  expaddzap  10694  expmul  10695  expmulzap  10696  m1expeven  10697  expsubap  10698  expp1zap  10699  expm1ap  10700  expdivap  10701  iexpcyc  10755  subsq2  10758  binom2  10762  binom21  10763  binom2sub  10764  binom2sub1  10765  mulbinom2  10767  binom3  10768  zesq  10769  bernneq  10771  sqoddm1div8  10804  mulsubdivbinom2ap  10822  nn0opthlem1d  10831  nn0opthd  10833  facp1  10841  facnn2  10845  faclbnd  10852  faclbnd6  10855  bcval  10860  bccmpl  10865  bcn0  10866  bcnn  10868  bcnp1n  10870  bcm1k  10871  bcp1n  10872  bcp1nk  10873  bcval5  10874  bcp1m1  10876  bcpasc  10877  bcn2m1  10880  bcn2p1  10881  omgadd  10913  hashunlem  10915  hashunsng  10918  hashdifsn  10930  hashxp  10937  zfz1isolemsplit  10949  zfz1isolem1  10951  zfz1iso  10952  seq3coll  10953  wrdf  10960  shftcan1  11018  shftcan2  11019  cjval  11029  cjth  11030  crre  11041  replim  11043  remim  11044  reim0b  11046  rereb  11047  mulreap  11048  cjreb  11050  recj  11051  reneg  11052  readd  11053  resub  11054  remullem  11055  imcj  11059  imneg  11060  imadd  11061  imsub  11062  cjcj  11067  cjadd  11068  ipcnval  11070  cjmulrcl  11071  cjneg  11074  addcj  11075  cjsub  11076  cnrecnv  11094  caucvgrelemcau  11164  cvg1nlemcau  11168  cvg1nlemres  11169  recvguniqlem  11178  resqrexlemover  11194  resqrexlemlo  11197  resqrexlemcalc1  11198  resqrexlemcalc3  11200  resqrexlemnm  11202  resqrexlemcvg  11203  absneg  11234  abscj  11236  sqabsadd  11239  sqabssub  11240  absmul  11253  absid  11255  absre  11261  absresq  11262  absexpzap  11264  recvalap  11281  abstri  11288  abs2dif2  11291  recan  11293  cau3lem  11298  amgm2  11302  bdtrilem  11423  xrmaxadd  11445  xrbdtri  11460  climaddc1  11513  climsubc1  11516  climcvg1nlem  11533  serf0  11536  summodclem3  11564  summodclem2a  11565  summodc  11567  fsumsplitsn  11594  fsumm1  11600  fsumsplitsnun  11603  fsump1  11604  isummulc2  11610  fsumrev  11627  fisum0diag2  11631  fsummulc2  11632  fsumsub  11636  fsumabs  11649  telfsumo  11650  fsumparts  11654  fsumrelem  11655  fsumiun  11661  binomlem  11667  binom  11668  binom1p  11669  binom11  11670  binom1dif  11671  bcxmas  11673  isumsplit  11675  isum1p  11676  divcnv  11681  arisum2  11683  trireciplem  11684  trirecip  11685  geolim  11695  georeclim  11697  geo2sum  11698  geo2lim  11700  geoisum1c  11704  0.999...  11705  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratz  11716  mertenslem2  11720  mertensabs  11721  clim2prod  11723  prodfrecap  11730  prodfdivap  11731  prodmodclem3  11759  prodmodclem2a  11760  fprodm1  11782  fprodp1  11784  fprodunsn  11788  fprodfac  11799  fprodeq0  11801  fprodconst  11804  fprodrec  11813  fproddivap  11814  fprodsplitsn  11817  ege2le3  11855  efaddlem  11858  efsub  11865  efexp  11866  eftlub  11874  efsep  11875  effsumlt  11876  ef4p  11878  tanval3ap  11898  resinval  11899  recosval  11900  efi4p  11901  efival  11916  efmival  11917  efeul  11918  sinadd  11920  cosadd  11921  tanaddap  11923  sinsub  11924  cossub  11925  sincossq  11932  sin2t  11933  cos2t  11934  cos2tsin  11935  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos12dec  11952  absef  11954  absefib  11955  efieq1re  11956  demoivreALT  11958  eirraplem  11961  dvdsexp  12045  oexpneg  12061  opeo  12081  omeo  12082  m1exp1  12085  flodddiv4  12120  flodddiv4t2lthalf  12123  bitsval  12127  bitsp1  12135  bitsinv1lem  12145  bitsinv1  12146  divgcdnnr  12170  gcdaddm  12178  gcdadd  12179  gcdid  12180  modgcd  12185  gcdmultipled  12187  dvdsgcdidd  12188  bezoutlemnewy  12190  bezoutlema  12193  bezoutlemb  12194  bezoutlemex  12195  bezoutlembz  12198  absmulgcd  12211  gcdmultiple  12214  gcdmultiplez  12215  rpmulgcd  12220  rplpwr  12221  eucalginv  12251  eucalg  12254  lcmneg  12269  lcmgcdlem  12272  lcmgcd  12273  lcmid  12275  lcm1  12276  mulgcddvds  12289  qredeq  12291  divgcdcoprmex  12297  prmind2  12315  rpexp1i  12349  pw2dvdslemn  12360  pw2dvdseulemle  12362  pw2dvdseu  12363  oddpwdclemxy  12364  oddpwdclemdvds  12365  oddpwdclemndvds  12366  oddpwdclemdc  12368  2sqpwodd  12371  nn0gcdsq  12395  phiprmpw  12417  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  fermltl  12429  prmdiv  12430  hashgcdlem  12433  odzdvds  12441  vfermltl  12447  modprm0  12450  nnnn0modprm0  12451  modprmn0modprm0  12452  coprimeprodsq  12453  pythagtriplem1  12461  pythagtriplem4  12464  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  pythagtriplem18  12477  pythagtrip  12479  pcpremul  12489  pceu  12491  pczpre  12493  pcdiv  12498  pcqmul  12499  pcqdiv  12503  pcexp  12505  pcxqcl  12508  pczdvds  12510  pczndvds  12512  pczndvds2  12514  pcid  12520  pcneg  12521  pcdvdstr  12523  pcgcd1  12524  pcgcd  12525  pc2dvds  12526  pcaddlem  12535  pcadd  12536  pcadd2  12537  pcmpt  12539  pcmpt2  12540  fldivp1  12544  pcfac  12546  pcbc  12547  expnprm  12549  prmpwdvds  12551  pockthlem  12552  pockthi  12554  4sqlem7  12580  4sqlem9  12582  4sqlem10  12583  4sqlem2  12585  4sqlem3  12586  4sqlem4  12588  mul4sqlem  12589  4sqlem11  12597  4sqlem16  12602  4sqlem17  12603  4sqlem19  12605  setscomd  12746  ressvalsets  12769  strressid  12776  ressval3d  12777  ressinbasd  12779  ressressg  12780  ressabsg  12781  grpinvalem  13089  grpinva  13090  grprida  13091  isnsgrp  13110  sgrpass  13112  sgrp1  13115  sgrppropd  13117  prdssgrpd  13119  mnd32g  13131  mnd4g  13133  mndpropd  13144  prdsidlem  13151  prdsmndd  13152  imasmnd2  13156  mhmex  13166  mhmlin  13171  gsumwmhm  13202  grprcan  13241  grpsubval  13250  grpinvid2  13257  grpasscan2  13268  grpsubinv  13277  grpinvadd  13282  grpsubid1  13289  grpsubadd0sub  13291  grpsubadd  13292  grpsubsub  13293  grpaddsubass  13294  grppncan  13295  grpnnncan2  13301  grpsubpropd2  13309  imasgrp2  13318  mhmlem  13322  mhmid  13323  mhmmnd  13324  ghmgrp  13326  mulgnn0gsum  13336  mulgnnp1  13338  mulgaddcomlem  13353  mulgaddcom  13354  mulginvinv  13356  mulgnn0dir  13360  mulgdirlem  13361  mulgp1  13363  mulgneg2  13364  mulgnn0ass  13366  mulgass  13367  mulgmodid  13369  mulgsubdir  13370  nmzsubg  13418  0nsg  13422  eqger  13432  qussub  13445  ghmlin  13456  ghmsub  13459  conjghm  13484  ablsub4  13521  abladdsub4  13522  ablsubsub4  13527  ablsub32  13530  ablnnncan  13531  gsumfzmptfidmadd2  13548  gsumfzconst  13549  gsumfzmhm2  13552  gsumfzsnfd  13553  mgpress  13565  rngass  13573  rngdi  13574  rngdir  13575  rngrz  13580  rngmneg2  13582  rngsubdi  13585  rngsubdir  13586  rngpropd  13589  imasrng  13590  srgass  13605  srgpcomp  13624  srgpcompp  13625  srgpcomppsc  13626  srg1expzeq1  13629  ringpropd  13672  ringrz  13678  ringnegr  13686  ringmneg2  13688  ringsubdi  13690  ringsubdir  13691  ring1  13693  imasring  13698  opprrng  13711  opprring  13713  mulgass3  13719  dvdsrd  13728  unitgrp  13750  invrfvald  13756  dvr1  13772  dvrass  13773  dvrcan1  13774  dvrcan3  13775  rdivmuldivd  13778  subrginv  13871  subrgdv  13872  resrhm2b  13883  islmod  13925  lmodlema  13926  islmodd  13927  lmodvs0  13956  lmodvneg1  13964  lmodvsubval2  13976  lmodsubvs  13977  lmodsubdi  13978  lmodsubdir  13979  lmodprop2d  13982  rmodislmodlem  13984  rmodislmod  13985  lsssn0  14004  sraval  14071  cnfldsub  14209  gsumfzfsumlem0  14220  gsumfzfsumlemm  14221  mulgrhm  14243  mulgrhm2  14244  znval  14270  znval2  14272  znunit  14293  psrval  14300  mplvalcoe  14324  mplval2g  14329  restabs  14519  cnprcl2k  14550  cnrest2r  14581  ispsmet  14667  psmettri2  14672  psmetsym  14673  ismet  14688  isxmet  14689  xmettri2  14705  xmetsym  14712  xmettri3  14718  mettri3  14719  xblss2ps  14748  xblss2  14749  comet  14843  xmetxp  14851  xmetxpbl  14852  txmetcnp  14862  fsumcncntop  14911  cncfi  14922  divcncfap  14958  limccl  15003  ellimc3apf  15004  limccnpcntop  15019  limccnp2lem  15020  reldvg  15023  dvfvalap  15025  eldvap  15026  dvcj  15053  dvfre  15054  dvexp  15055  dvexp2  15056  dvrecap  15057  dvmptaddx  15063  dvmptmulx  15064  dvmptnegcn  15066  dvmptsubcn  15067  dvmptcjx  15068  dvmptfsum  15069  dveflem  15070  dvef  15071  plyconst  15089  plyaddlem1  15091  plymullem1  15092  plyadd  15095  plymul  15096  plycoeid3  15101  plycolemc  15102  plyco  15103  plycjlemc  15104  plycj  15105  plyrecj  15107  dvply1  15109  dvply2g  15110  sin0pilem1  15125  sin0pilem2  15126  efper  15151  sinperlem  15152  efimpi  15163  ptolemy  15168  tangtx  15182  abssinper  15190  cosq34lt1  15194  rpcxpef  15238  rpcxpp1  15250  rpcxpneg  15251  rpcxpsub  15252  rpmulcxp  15253  rpdivcxp  15255  cxpmul  15256  rpcxpmul2  15257  rpcxproot  15258  cxpcom  15282  rpabscxpbnd  15284  rplogbval  15289  rplogbreexp  15297  rplogbzexp  15298  rprelogbmulexp  15300  rprelogbdiv  15301  relogbexpap  15302  rplogbcxp  15307  rpcxplogb  15308  logbgcd1irr  15311  logbgcd1irraplemap  15313  binom4  15323  wilthlem1  15324  sgmval  15327  sgmppw  15336  1sgmprm  15338  mersenne  15341  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgslem1  15349  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsval4  15369  lgsneg  15373  lgsneg1  15374  lgsmod  15375  lgsdir2  15382  lgsdirprm  15383  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  lgssq2  15390  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem2  15411  gausslemma2dlem3  15412  gausslemma2dlem4  15413  gausslemma2dlem5  15415  gausslemma2dlem6  15416  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  lgsquad2lem2  15431  lgsquad2  15432  lgsquad3  15433  m1lgs  15434  2lgslem3c  15444  2lgslem3d  15445  2lgslem3d1  15449  2sqlem2  15464  2sqlem3  15466  2sqlem4  15467  2sqlem8  15472  2sqlem9  15473  2sqlem10  15474  qdencn  15784  trilpolemclim  15793  trilpolemcl  15794  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  trilpo  15800  apdifflemf  15803  apdiff  15805  iswomni0  15808  redcwlpolemeq1  15811  redcwlpo  15812  nconstwlpolem0  15820  nconstwlpolemgt0  15821  nconstwlpo  15823  neapmkv  15825