Theorem oveq2d 6091

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

Syntax hints:   → wi 4   = wceq 1402  (class class class)co 6075

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  csbov1g  6116  caovassg  6238  caovdig  6254  caovdirg  6257  caov32d  6260  caov4d  6264  caov42d  6266  suppofss1dcl  6494  suppofss2dcl  6495  nnaass  6748  nndi  6749  nnmass  6750  nnmsucr  6751  ecovass  6908  ecoviass  6909  ecovdi  6910  ecovidi  6911  addasspig  7687  mulasspig  7689  distrpig  7690  dfplpq2  7711  mulpipq2  7728  addassnqg  7739  prarloclemarch  7775  prarloclemarch2  7776  ltrnqg  7777  enq0sym  7789  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  nq0a0  7814  distrnq0  7816  addassnq0  7819  prarloclemlo  7851  prarloclem3  7854  prarloclem5  7857  prarloclemcalc  7859  addnqprl  7886  addnqpru  7887  prmuloclemcalc  7922  mulnqprl  7925  mulnqpru  7926  distrlem4prl  7941  distrlem4pru  7942  1idprl  7947  1idpru  7948  ltexprlemloc  7964  addcanprleml  7971  addcanprlemu  7972  recexprlem1ssu  7991  ltmprr  7999  caucvgprlemcanl  8001  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlemlim  8018  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgpr  8039  caucvgprprlemell  8042  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkeqj  8047  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexb  8064  caucvgprprlemaddq  8065  caucvgprprlem1  8066  addcmpblnr  8096  mulcmpblnrlemg  8097  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  ltsrprg  8104  recexgt0sr  8130  mulgt0sr  8135  caucvgsrlemgt1  8152  caucvgsrlemoffval  8153  caucvgsr  8159  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  suplocsr  8166  mulcnsr  8192  pitoregt0  8206  recidpirqlemcalc  8214  axmulcom  8228  axmulass  8230  axdistr  8231  ax0id  8235  axcnre  8238  recriota  8247  axcaucvglemcau  8255  axcaucvglemres  8256  mulrid  8313  adddirp1d  8342  mul32  8446  mul31  8447  add32  8475  add4  8477  add42  8478  cnegex  8494  addcan2  8497  addsubass  8526  subsub2  8544  nppcan2  8547  sub32  8550  nnncan  8551  sub4  8561  muladd  8701  subdi  8702  mul2neg  8715  submul2  8716  mulsub  8718  muls1d  8735  mulsubfacd  8736  add20  8792  recexre  8896  rereim  8904  apreap  8905  ltmul1  8910  cru  8920  apreim  8921  mulreim  8922  apadd1  8926  apneg  8929  mulap0  8972  divrecap  9008  divassap  9010  divmulasscomap  9016  divsubdirap  9028  divdivdivap  9033  divmul24ap  9036  divmuleqap  9037  divcanap6  9039  divdivap1  9043  divdivap2  9044  divsubdivap  9048  conjmulap  9049  div2negap  9055  apmul1  9108  cju  9281  nnmulcl  9304  add1p1  9534  sub1m1  9535  cnm2m1cnm3  9536  xp1d2m1eqxm1d2  9537  div4p1lem1div2  9538  un0addcl  9575  un0mulcl  9576  zaddcllemneg  9662  qapne  10018  cnref1o  10030  rexsub  10234  xnegid  10240  xaddcom  10242  xnegdi  10249  xaddass  10250  xaddass2  10251  xpncan  10252  xnpcan  10253  xleadd1a  10254  xsubge0  10262  xposdif  10263  xlesubadd  10264  xadd4d  10266  lincmb01cmp  10384  iccf1o  10386  ige3m2fz  10432  fztp  10463  fzsuc2  10464  fseq1m1p1  10480  fzm1  10485  ige2m1fz1  10494  nn0split  10521  nnsplit  10522  fzo0addelr  10585  elfzoext  10588  fzval3  10600  zpnn0elfzo1  10604  fzosplitsnm1  10605  fzosplitpr  10630  fzosplitprm1  10631  fzoshftral  10635  rebtwn2zlemstep  10665  flhalf  10715  fldiv4lem1div2uz2  10719  modqval  10739  modqvalr  10740  modqdiffl  10750  modqfrac  10752  flqmod  10753  intqfrac  10754  zmod10  10755  modqmulnn  10757  modqvalp1  10758  modqid  10764  modqcyc  10774  modqcyc2  10775  modqmul1  10792  q2submod  10800  modqdi  10807  modqsubdir  10808  modqeqmodmin  10809  modsumfzodifsn  10811  addmodlteq  10813  frecuzrdgsuctlem  10838  uzsinds  10859  seqeq3  10867  iseqvalcbv  10874  seq3val  10875  seqvalcd  10876  seqf  10879  seq3p1  10880  seqovcd  10882  seqp1cd  10885  seq3m1  10888  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  monoord2  10901  ser3mono  10902  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  seq3caopr2  10908  seqcaopr2g  10909  seq3caopr  10910  seqcaoprg  10911  seqf1oglem2a  10933  seqf1oglem2  10935  seq3id2  10941  seq3homo  10942  seq3z  10943  seqhomog  10945  exp3vallem  10955  exp3val  10956  expp1  10961  expnegap0  10962  expineg2  10963  expn1ap0  10964  expm1t  10982  1exp  10983  expnegzap  10988  mulexpzap  10994  expadd  10996  expaddzaplem  10997  expaddzap  10998  expmul  10999  expmulzap  11000  m1expeven  11001  expsubap  11002  expp1zap  11003  expm1ap  11004  expdivap  11005  iexpcyc  11059  subsq2  11062  binom2  11066  binom21  11067  binom2sub  11068  binom2sub1  11069  mulbinom2  11071  binom3  11072  zesq  11074  bernneq  11076  sqoddm1div8  11109  mulsubdivbinom2ap  11127  nn0opthlem1d  11136  nn0opthd  11138  facp1  11146  facnn2  11150  faclbnd  11157  faclbnd6  11160  bcval  11165  bccmpl  11170  bcn0  11171  bcnn  11173  bcnp1n  11175  bcm1k  11176  bcp1n  11177  bcp1nk  11178  bcval5  11179  bcp1m1  11181  bcpasc  11182  bcm1n  11185  bcn2m1  11186  bcn2p1  11187  omgadd  11220  hashunlem  11222  hashunsng  11226  hashdifsn  11238  hashxp  11245  hashmap  11246  sseqn  11257  hashf1lem2  11264  hashf1  11265  hashfac  11266  zfz1isolemsplit  11268  zfz1isolem1  11270  zfz1iso  11271  seq3coll  11272  wrdf  11288  ccatfvalfi  11338  elfzelfzccat  11346  ccatlid  11352  ccatrid  11353  ccatass  11354  ccatalpha  11359  ccatws1leng  11380  ccats1val2  11386  ccatw2s1p1g  11391  swrdval  11398  swrd00g  11399  swrdf  11405  swrdfv2  11413  swrdwrdsymbg  11414  swrdspsleq  11417  swrds1  11418  swrdlsw  11419  ccatswrd  11420  swrdccat2  11421  pfxmpt  11430  pfxfv  11434  pfxeq  11446  pfxsuff1eqwrdeq  11449  ccatpfx  11451  pfxccat1  11452  swrdswrd  11455  pfxswrd  11456  swrdpfx  11457  pfxpfx  11458  pfxlswccat  11463  ccats1pfxeq  11464  ccats1pfxeqrex  11465  ccatopth2  11467  cats1un  11471  wrdind  11472  wrd2ind  11473  swrdccatfn  11474  swrdccatin1  11475  pfxccatin12lem4  11476  swrdccatin2  11479  pfxccatin12lem2c  11480  pfxccatin12lem2  11481  pfxccatin12  11483  swrdccat  11485  swrdccat3blem  11489  swrdccat3b  11490  swrdccatin2d  11494  pfxccatin12d  11495  reuccatpfxs1lem  11496  reuccatpfxs1  11497  shftcan1  11577  shftcan2  11578  cjval  11588  cjth  11589  crre  11600  replim  11602  remim  11603  reim0b  11605  rereb  11606  mulreap  11607  cjreb  11609  recj  11610  reneg  11611  readd  11612  resub  11613  remullem  11614  imcj  11618  imneg  11619  imadd  11620  imsub  11621  cjcj  11626  cjadd  11627  ipcnval  11629  cjmulrcl  11630  cjneg  11633  addcj  11634  cjsub  11635  sq01  11638  cnrecnv  11654  caucvgrelemcau  11724  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniqlem  11738  resqrexlemover  11754  resqrexlemlo  11757  resqrexlemcalc1  11758  resqrexlemcalc3  11760  resqrexlemnm  11762  resqrexlemcvg  11763  absneg  11794  abscj  11796  sqabsadd  11799  sqabssub  11800  absmul  11813  absid  11815  absre  11821  absresq  11822  absexpzap  11824  recvalap  11841  abstri  11848  abs2dif2  11851  recan  11853  cau3lem  11858  amgm2  11862  bdtrilem  11983  xrmaxadd  12005  xrbdtri  12020  climaddc1  12073  climsubc1  12076  climcvg1nlem  12093  serf0  12096  fzf1o  12120  summodclem3  12125  summodclem2a  12126  summodc  12128  fsumsplitsn  12155  fsumm1  12161  fsumsplitsnun  12164  fsump1  12165  isummulc2  12171  fsumrev  12188  fisum0diag2  12192  fsummulc2  12193  fsumsub  12197  fsumabs  12210  telfsumo  12211  fsumparts  12215  fsumrelem  12216  fsumiun  12222  binomlem  12228  binom  12229  binom1p  12230  binom11  12231  binom1dif  12232  bcxmas  12234  isumsplit  12236  isum1p  12237  divcnv  12242  arisum2  12244  trireciplem  12245  trirecip  12246  geolim  12256  georeclim  12258  geo2sum  12259  geo2lim  12261  geoisum1c  12265  0.999...  12266  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratz  12277  mertenslem2  12281  mertensabs  12282  clim2prod  12284  prodfrecap  12291  prodfdivap  12292  prodmodclem3  12320  prodmodclem2a  12321  fprodm1  12343  fprodp1  12345  fprodunsn  12349  fprodfac  12360  fprodeq0  12362  fprodconst  12365  fprodrec  12374  fproddivap  12375  fprodsplitsn  12378  ege2le3  12416  efaddlem  12419  efsub  12426  efexp  12427  eftlub  12435  efsep  12436  effsumlt  12437  ef4p  12439  tanval3ap  12459  resinval  12460  recosval  12461  efi4p  12462  efival  12477  efmival  12478  efeul  12479  sinadd  12481  cosadd  12482  tanaddap  12484  sinsub  12485  cossub  12486  sincossq  12493  sin2t  12494  cos2t  12495  cos2tsin  12496  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos12dec  12513  absef  12515  absefib  12516  efieq1re  12517  demoivreALT  12519  eirraplem  12522  dvdsexp  12606  oexpneg  12622  opeo  12642  omeo  12643  m1exp1  12646  flodddiv4  12681  flodddiv4t2lthalf  12684  bitsval  12688  bitsp1  12696  bitsinv1lem  12706  bitsinv1  12707  divgcdnnr  12731  gcdaddm  12739  gcdadd  12740  gcdid  12741  modgcd  12746  gcdmultipled  12748  dvdsgcdidd  12749  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  bezoutlemex  12756  bezoutlembz  12759  absmulgcd  12772  gcdmultiple  12775  gcdmultiplez  12776  rpmulgcd  12781  rplpwr  12782  eucalginv  12812  eucalg  12815  lcmneg  12830  lcmgcdlem  12833  lcmgcd  12834  lcmid  12836  lcm1  12837  mulgcddvds  12850  qredeq  12852  divgcdcoprmex  12858  prmind2  12876  rpexp1i  12910  pw2dvdslemn  12921  pw2dvdseulemle  12923  pw2dvdseu  12924  oddpwdclemxy  12925  oddpwdclemdvds  12926  oddpwdclemndvds  12927  oddpwdclemdc  12929  2sqpwodd  12932  nn0gcdsq  12956  phiprmpw  12978  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  fermltl  12990  prmdiv  12991  hashgcdlem  12994  odzdvds  13002  vfermltl  13008  modprm0  13011  nnnn0modprm0  13012  modprmn0modprm0  13013  coprimeprodsq  13014  pythagtriplem1  13022  pythagtriplem4  13025  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem16  13036  pythagtriplem18  13038  pythagtrip  13040  pcpremul  13050  pceu  13052  pczpre  13054  pcdiv  13059  pcqmul  13060  pcqdiv  13064  pcexp  13066  pcxqcl  13069  pczdvds  13071  pczndvds  13073  pczndvds2  13075  pcid  13081  pcneg  13082  pcdvdstr  13084  pcgcd1  13085  pcgcd  13086  pc2dvds  13087  pcaddlem  13096  pcadd  13097  pcadd2  13098  pcmpt  13100  pcmpt2  13101  fldivp1  13105  pcfac  13107  pcbc  13108  expnprm  13110  prmpwdvds  13112  pockthlem  13113  pockthi  13115  4sqlem7  13141  4sqlem9  13143  4sqlem10  13144  4sqlem2  13146  4sqlem3  13147  4sqlem4  13149  mul4sqlem  13150  4sqlem11  13158  4sqlem16  13163  4sqlem17  13164  4sqlem19  13166  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemsv  13231  ballotfilemsima  13237  ballotfilemfrci  13249  setscomd  13371  ressvalsets  13395  strressid  13402  ressval3d  13403  ressinbasd  13405  ressressg  13406  ressabsg  13407  grpinvalem  13682  grpinva  13683  grprida  13684  isnsgrp  13698  sgrpass  13700  sgrp1  13703  sgrppropd  13705  mnd32g  13717  mnd4g  13719  mndpropd  13730  imasmnd2  13736  mhmex  13746  mhmlin  13751  gzsumwmhm  13780  grprcan  13819  grpsubval  13828  grpinvid2  13835  grpasscan2  13846  grpsubinv  13855  grpinvadd  13860  grpsubid1  13867  grpsubadd0sub  13869  grpsubadd  13870  grpsubsub  13871  grpaddsubass  13872  grppncan  13873  grpnnncan2  13879  grpsubpropd2  13887  imasgrp2  13890  mhmlem  13894  mhmid  13895  mhmmnd  13896  ghmgrp  13898  mulgnn0gzsum  13908  mulgnnp1  13910  mulgaddcomlem  13925  mulgaddcom  13926  mulginvinv  13928  mulgnn0dir  13932  mulgdirlem  13933  mulgp1  13935  mulgneg2  13936  mulgnn0ass  13938  mulgass  13939  mulgmodid  13941  mulgsubdir  13942  nmzsubg  13990  0nsg  13994  eqger  14004  qussub  14017  ghmlin  14028  ghmsub  14031  conjghm  14056  ablsub4  14094  abladdsub4  14095  ablsubsub4  14100  ablsub32  14103  ablnnncan  14104  gzsumconst  14120  gzsummhm2  14123  gzsumsnfd  14124  gzsumsplit0  14125  gsumvalfi  14129  gzsumgsum1  14130  gzsumgsum  14132  gsumsncmn  14133  gsump1  14134  gsumzfi  14135  gsumclfi  14136  gsumf1ofi  14137  gsummptfidmadd  14138  gsummptfidmadd2  14139  gsumsubmclfi  14140  gsummhm2fi  14142  gsumconstcmn  14143  prdssgrpd  14168  prdsidlem  14170  prdsmndd  14171  mgpress  14205  rngass  14213  rngdi  14214  rngdir  14215  rngrz  14220  rngmneg2  14222  rngsubdi  14225  rngsubdir  14226  rngpropd  14229  imasrng  14230  srgass  14249  srgpcomp  14268  srgpcompp  14269  srgpcomppsc  14270  srg1expzeq1  14273  ringpropd  14316  ringrz  14322  ringnegr  14330  ringmneg2  14332  ringsubdi  14334  ringsubdir  14335  ring1  14337  imasring  14342  opprrng  14355  opprring  14357  mulgass3  14364  dvdsrd  14374  unitgrp  14396  invrfvald  14402  dvr1  14418  dvrass  14419  dvrcan1  14420  dvrcan3  14421  rdivmuldivd  14424  subrginv  14518  subrgdv  14519  resrhm2b  14530  rrgsupp  14547  islmod  14600  lmodlema  14601  islmodd  14602  lmodvs0  14631  lmodvneg1  14639  lmodvsubval2  14651  lmodsubvs  14652  lmodsubdi  14653  lmodsubdir  14654  lmodprop2d  14657  rmodislmodlem  14659  rmodislmod  14660  lsssn0  14679  sraval  14746  cnfldsub  14884  gsumfsum  14895  mulgrhm  14916  mulgrhm2  14917  znval  14943  znval2  14945  znunit  14966  psrval  14973  mplvalcoe  15004  mplval2g  15009  restabs  15199  cnprcl2k  15230  cnrest2r  15261  ispsmet  15347  psmettri2  15352  psmetsym  15353  ismet  15368  isxmet  15369  xmettri2  15385  xmetsym  15392  xmettri3  15398  mettri3  15399  xblss2ps  15428  xblss2  15429  comet  15523  xmetxp  15531  xmetxpbl  15532  txmetcnp  15542  fsumcncntop  15591  cncfi  15602  divcncfap  15638  limccl  15683  ellimc3apf  15684  limccnpcntop  15699  limccnp2lem  15700  reldvg  15703  dvfvalap  15705  eldvap  15706  dvcj  15733  dvfre  15734  dvexp  15735  dvexp2  15736  dvrecap  15737  dvmptaddx  15743  dvmptmulx  15744  dvmptnegcn  15746  dvmptsubcn  15747  dvmptcjx  15748  dvmptfsum  15749  dveflem  15750  dvef  15751  plyconst  15769  plyaddlem1  15771  plymullem1  15772  plyadd  15775  plymul  15776  plycoeid3  15781  plycolemc  15782  plyco  15783  plycjlemc  15784  plycj  15785  plyrecj  15787  dvply1  15789  dvply2g  15790  sin0pilem1  15805  sin0pilem2  15806  efper  15831  sinperlem  15832  efimpi  15843  ptolemy  15848  tangtx  15862  abssinper  15870  cosq34lt1  15874  rpcxpef  15919  rpcxpp1  15931  rpcxpneg  15932  rpcxpsub  15933  rpmulcxp  15934  rpdivcxp  15936  cxpmul  15937  rpcxpmul2  15938  rpcxproot  15939  cxpcom  15963  rpabscxpbnd  15965  rplogbval  15970  rplogbreexp  15978  rplogbzexp  15979  rprelogbmulexp  15981  rprelogbdiv  15982  relogbexpap  15983  rplogbcxp  15988  rpcxplogb  15989  logbgcd1irr  15992  logbgcd1irraplemap  15994  binom4  16004  pellexlem2  16006  pellexlem3  16007  wilthlem1  16008  sgmval  16011  sgmppw  16020  1sgmprm  16022  mersenne  16025  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgslem1  16033  lgsval  16037  lgsfvalg  16038  lgsval2lem  16043  lgsval4  16053  lgsneg  16057  lgsneg1  16058  lgsmod  16059  lgsdir2  16066  lgsdirprm  16067  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgssq2  16074  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem2  16095  gausslemma2dlem3  16096  gausslemma2dlem4  16097  gausslemma2dlem5  16099  gausslemma2dlem6  16100  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem1  16114  lgsquad2lem2  16115  lgsquad2  16116  lgsquad3  16117  m1lgs  16118  2lgslem3c  16128  2lgslem3d  16129  2lgslem3d1  16133  2sqlem2  16148  2sqlem3  16150  2sqlem4  16151  2sqlem8  16156  2sqlem9  16157  2sqlem10  16158  vtxdumgrfival  16453  p1evtxdeqfi  16467  p1evtxdp1fi  16468  iswlk  16478  upgr2wlkdc  16532  wlkres  16534  trlreslem  16544  isclwwlk  16549  clwwlkccatlem  16555  clwwlknp  16572  clwwlkn1  16573  clwwlkn2  16576  clwwlkext2edg  16577  clwwlknonex2lem1  16592  clwwlknonex2lem2  16593  clwwlknonex2  16594  iseupth  16602  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  depindlem1  16661  qdencn  16977  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  trilpo  16997  apdifflemf  17000  apdiff  17002  iswomni0  17006  redcwlpolemeq1  17009  redcwlpo  17010  nconstwlpolem0  17018  nconstwlpolemgt0  17019  nconstwlpo  17021  neapmkv  17023