Theorem oveqd 6987

Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveqd	⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq 6976	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1507  (class class class)co 6970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-rex 3088  df-uni 4707  df-br 4924  df-iota 6146  df-fv 6190  df-ov 6973

This theorem is referenced by:  oveq123d  6991  oveqdr  6998  csbov  7012  csbov12g  7013  ovmpodxf  7110  oprssov  7127  2mpo0  7206  ofeq  7223  mptmpoopabbrd  7579  mptmpoopabovd  7580  el2mpocsbcl  7581  fnmpoovd  7583  ruclem1  15434  vdwapval  16155  vdwapid1  16157  vdwmc2  16161  vdwpc  16162  vdwlem5  16167  vdwlem8  16170  vdwlem13  16175  prdsval  16574  prdsdsval2  16603  pwsplusgval  16609  pwsmulrval  16610  pwsvscafval  16613  imasval  16630  iscat  16791  iscatd  16792  catidex  16793  catideu  16794  cidfval  16795  cidval  16796  catidd  16799  iscatd2  16800  catlid  16802  catrid  16803  homffval  16808  homfeqd  16813  homfeqval  16815  comfffval  16816  comffval  16817  comfeq  16824  comfeqd  16825  comfeqval  16826  catpropd  16827  oppcval  16831  oppcco  16835  monfval  16850  ismon  16851  oppcmon  16856  oppcepi  16857  sectffval  16868  sectfval  16869  invffval  16876  isoval  16883  dfiso2  16890  isofn  16893  invisoinvl  16908  invcoisoid  16910  isocoinvid  16911  issubc  16953  issubc3  16967  isfunc  16982  cofuval  17000  cofuval2  17005  funcres  17014  funcres2b  17015  funcres2  17016  funcres2c  17019  isfull  17028  isfth  17032  fullres2c  17057  natfval  17064  isnat  17065  fucval  17076  fucco  17080  fucpropd  17095  initoval  17105  termoval  17106  homarcl  17136  coafval  17172  resssetc  17200  resscatc  17213  catciso  17215  xpcval  17275  1stfval  17289  2ndfval  17292  prfval  17297  prfcl  17301  evlfval  17315  curfval  17321  curf1cl  17326  curfcl  17330  uncf1  17334  uncf2  17335  diag12  17342  diag2  17343  curf2ndf  17345  hofval  17350  hof1  17352  hof2fval  17353  hofcl  17357  yon12  17363  yon2  17364  hofpropd  17365  joinval  17463  meetval  17477  isdlat  17651  plusffval  17705  issstrmgm  17710  grpidval  17718  grpidd  17726  gsumvalx  17728  gsumpropd  17730  gsumress  17734  ismndd  17771  issubmnd  17776  submnd0  17778  ismhm  17795  issubm  17805  resmhm  17817  resmhm2  17818  resmhm2b  17819  isgrp  17887  isgrpd2e  17900  grpidd2  17918  grpinvfval  17919  grpinvfvalALT  17920  imasgrp2  17991  imasgrp  17992  subg0  18059  subginv  18060  subgcl  18063  issubgrpd2  18069  isnsg  18082  isghm  18119  resghm  18135  isga  18182  subgga  18191  gasubg  18193  cntzfval  18211  resscntz  18223  odfval  18412  odfvalALT  18413  gexval  18454  lsmfval  18514  lsmvalx  18515  oppglsm  18518  subglsm  18547  pj1fval  18568  efgtval  18597  iscmn  18663  iscmnd  18668  submcmn2  18707  iscyg  18744  issrg  18970  isring  19014  ringidss  19040  prdsmgp  19073  mulgass3  19100  dvdsrval  19108  isirred  19162  isdrngd  19240  isdrngrd  19241  subrg1  19258  subrgmcl  19260  subrgdvds  19262  subrguss  19263  subrginv  19264  subrgdv  19265  subrgunit  19266  subrgugrp  19267  abvfval  19301  isabvd  19303  issrngd  19344  islmod  19350  islmodd  19352  scaffval  19364  lmodpropd  19409  lssset  19417  islssd  19419  prdslmodd  19453  islmhm  19511  reslmhm  19536  reslmhm2  19537  reslmhm2b  19538  islbs  19560  rlmvneg  19691  rrgval  19771  isassa  19799  isassad  19807  assamulgscmlem2  19833  psrval  19846  resspsradd  19900  resspsrmul  19901  resspsrvsca  19902  mplmon2mul  19984  ply1coe  20157  lply1binomsc  20168  evl1expd  20200  evl1scvarpw  20218  isphl  20464  ipffval  20484  isphld  20490  phssipval  20493  phssip  20494  phlssphl  20495  ocvfval  20502  isobs  20556  frlmplusgval  20600  frlmsubgval  20601  frlmvscafval  20602  frlmip  20614  frlmipval  20615  frlmup1  20634  lsslindf  20666  mamufval  20688  matplusg2  20730  matvsca2  20731  matplusgcell  20736  matsubgcell  20737  matinvgcell  20738  matvscacell  20739  matmulcell  20748  mpomatmul  20749  mat1  20750  mattposm  20762  mat1dimmul  20779  dmatmul  20800  dmatcrng  20805  scmataddcl  20819  scmatsubcl  20820  scmatcrng  20824  smatvscl  20827  scmatghm  20836  scmatmhm  20837  mvmulfval  20845  ma1repveval  20874  mdetrlin  20905  mdetrsca  20906  mdetmul  20926  madurid  20947  minmar1cl  20954  smadiadetglem1  20974  smadiadetr  20978  matinv  20980  slesolinv  20983  slesolinvbi  20984  cramerimplem3  20988  cpmatacl  21018  mat2pmatghm  21032  decpmatmullem  21073  decpmatmul  21074  pmatcollpw1lem1  21076  pmatcollpw2lem  21079  pmatcollpwlem  21082  pmatcollpw3lem  21085  mply1topmatval  21106  mp2pm2mplem1  21108  mp2pm2mplem4  21111  mp2pm2mplem5  21112  mp2pm2mp  21113  chpmat1d  21138  chpscmatgsummon  21147  chfacfpmmulgsum2  21167  xkocnv  22116  submtmd  22406  prdsdsf  22670  ressprdsds  22674  blfvalps  22686  prdsxmslem2  22832  tmsxpsval  22841  ngpds  22906  sgrimval  22934  subgngp  22937  tngngp  22956  tngngp3  22958  isnlm  22977  lssnlm  23003  isphtpy  23278  isphtpc  23291  pi1cpbl  23341  pi1addf  23344  pi1addval  23345  pi1grplem  23346  clmsub  23377  clmvsass  23386  clmvsdir  23388  isclmp  23394  cvsdiv  23429  iscph  23467  cphdir  23502  cphdi  23503  cph2di  23504  cph2subdi  23507  cphass  23508  tcphval  23514  ipcau2  23530  tcphcphlem1  23531  tcphcphlem2  23532  cphsscph  23547  caufval  23571  rrxip  23686  rrxvsca  23690  rrxplusgvscavalb  23691  rrxdsfival  23709  ehleudisval  23715  dvlip2  24285  q1pval  24440  r1pval  24443  dvntaylp  24652  efabl  24825  efsubm  24826  dchrmul  25516  istrkgc  25932  istrkgb  25933  istrkgcb  25934  istrkge  25935  istrkgl  25936  istrkgld  25937  iscgrg  25990  isismt  26012  tglngval  26029  legval  26062  ishlg  26080  mirval  26133  israg  26175  ishpg  26237  lmif  26263  islmib  26265  isinag  26317  ttgval  26354  wksonproplem  27184  wspthsnon  27328  iswwlksnon  27329  iswspthsnon  27332  isconngr  27708  isconngr1  27709  grpodivval  28079  dipfval  28246  ipval  28247  sspgval  28273  sspsval  28275  lnoval  28296  ajfval  28353  dipdir  28386  dipass  28389  htth  28464  isomnd  30398  submomnd  30407  inftmrel  30431  isinftm  30432  isslmd  30452  rngurd  30492  rdivmuldivd  30497  isorng  30507  suborng  30523  resv1r  30545  drgextlsp  30581  fedgmullem1  30610  fedgmullem2  30611  fedgmul  30612  extdg1id  30638  smatlem  30661  submatminr1  30674  metidval  30731  pstmval  30736  pstmfval  30737  zlm0  30804  zlm1  30805  sitmval  31209  breprexp  31513  istrkg2d  31546  afsval  31551  mclsrcl  32268  mppsval  32279  frecseq123  32580  matunitlindflem2  34278  istotbnd  34437  isbnd  34448  rrnequiv  34503  isrngo  34565  rngohomval  34632  idlval  34681  pridlval  34701  lflset  35588  islfld  35591  ldualvadd  35658  ldualsmul  35664  ldualvs  35666  isopos  35709  cmtfvalN  35739  iscvlat  35852  ishlat1  35881  lineset  36267  psubspset  36273  paddfval  36326  paddval  36327  ltrnfset  36646  trnfsetN  36684  trlfset  36689  tgrpov  37277  erngplus  37332  erngmul  37335  erngplus-rN  37340  erngmul-rN  37343  erngdvlem3  37519  erngdvlem4  37520  erng0g  37523  erngdvlem3-rN  37527  erngdvlem4-rN  37528  dvaplusg  37538  dvamulr  37541  dvavadd  37544  dvavsca  37546  dvalveclem  37554  dvhmulr  37615  dvhfvadd  37620  dvhvadd  37621  dvhopvadd2  37623  dvhvaddcl  37624  dvhvaddcomN  37625  dvhvsca  37630  dvhlveclem  37637  dvh0g  37640  djavalN  37664  diblsmopel  37700  dicvaddcl  37719  cdlemn6  37731  dihffval  37759  dihopelvalcpre  37777  djhval  37927  lcdvaddval  38127  lcdsmul  38131  lcdvsval  38133  lcdlkreq2N  38152  hvmapffval  38287  hvmapfval  38288  hdmap1fval  38325  hgmapffval  38414  hgmapfval  38415  hgmapadd  38423  hlhilipval  38478  hlhilhillem  38489  prjspval  38605  ioorrnopnlem  41966  hoidmvval0b  42249  hoidmvlelem2  42255  hoidmvlelem3  42256  hoidmvle  42259  ovnhoi  42262  hoiqssbl  42284  hspmbllem2  42286  vonioo  42341  vonicc  42344  ismgmd  43351  ismgmhm  43358  issubmgm  43364  resmgmhm  43373  resmgmhm2  43374  resmgmhm2b  43375  idfusubc  43441  rnghmval  43466  lidlmsgrp  43501  lidlrng  43502  zlidlring  43503  uzlidlring  43504  rnghmresel  43539  rngchom  43542  rngcco  43546  rnghmsubcsetclem1  43550  rhmresel  43585  ringchom  43588  ringcco  43592  rhmsubcsetclem1  43596  rhmsubcrngclem1  43602  irinitoringc  43644  ovmpt2rdxf  43691  lincop  43770  lincval  43771  lincsum  43791  lincscm  43792  lmod1lem2  43850  lmod1lem3  43851  lmod1lem4  43852  ldepsnlinc  43870  lines  44026  line  44027  rrxlines  44028  rrxline  44029  spheres  44041