Theorem oveqd 7230

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 7219	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1543  (class class class)co 7213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-br 5054  df-iota 6338  df-fv 6388  df-ov 7216

This theorem is referenced by:  oveq123d  7234  oveqdr  7241  csbov  7256  csbov12g  7257  ovmpodxf  7359  oprssov  7377  2mpo0  7454  ofeq  7471  mptmpoopabbrd  7851  mptmpoopabovd  7852  el2mpocsbcl  7853  fnmpoovd  7855  frecseq123  8024  ruclem1  15792  vdwapval  16526  vdwapid1  16528  vdwmc2  16532  vdwpc  16533  vdwlem5  16538  vdwlem8  16541  vdwlem13  16546  prdsval  16960  prdsdsval2  16989  pwsplusgval  16995  pwsmulrval  16996  pwsvscafval  16999  imasval  17016  iscat  17175  iscatd  17176  catidex  17177  catideu  17178  cidfval  17179  cidval  17180  catidd  17183  iscatd2  17184  catlid  17186  catrid  17187  homffval  17193  homfeqd  17198  homfeqval  17200  comfffval  17201  comffval  17202  comfeq  17209  comfeqd  17210  comfeqval  17211  catpropd  17212  oppcval  17216  oppcco  17221  monfval  17237  ismon  17238  oppcmon  17243  oppcepi  17244  sectffval  17255  sectfval  17256  invffval  17263  isoval  17270  dfiso2  17277  isofn  17280  invisoinvl  17295  invcoisoid  17297  isocoinvid  17298  issubc  17341  issubc3  17355  isfunc  17370  cofuval  17388  cofuval2  17393  funcres  17402  funcres2b  17403  funcres2  17404  funcres2c  17408  isfull  17417  isfth  17421  fullres2c  17446  natfval  17453  isnat  17454  fucval  17466  fucco  17471  fucpropd  17486  initoval  17499  termoval  17500  homarcl  17534  coafval  17570  resssetc  17598  resscatc  17615  catciso  17617  xpcval  17684  1stfval  17698  2ndfval  17701  prfval  17706  prfcl  17710  evlfval  17725  curfval  17731  curf1cl  17736  curfcl  17740  uncf1  17744  uncf2  17745  diag12  17752  diag2  17753  curf2ndf  17755  hofval  17760  hof1  17762  hof2fval  17763  hofcl  17767  yon12  17773  yon2  17774  hofpropd  17775  joinval  17883  meetval  17897  isdlat  18028  plusffval  18120  issstrmgm  18125  grpidval  18133  grpidd  18143  gsumvalx  18148  gsumpropd  18150  gsumress  18154  ismndd  18195  issubmnd  18200  submnd0  18202  ismhm  18220  issubm  18230  resmhm  18247  resmhm2  18248  resmhm2b  18249  isgrp  18371  isgrpd2e  18386  grpidd2  18405  grpinvfval  18406  grpinvfvalALT  18407  imasgrp2  18478  imasgrp  18479  subg0  18549  subginv  18550  subgcl  18553  issubgrpd2  18559  isnsg  18571  isghm  18622  resghm  18638  isga  18685  subgga  18694  gasubg  18696  cntzfval  18714  resscntz  18726  odfval  18924  odfvalALT  18925  gexval  18967  lsmfval  19027  lsmvalx  19028  oppglsm  19031  subglsm  19063  pj1fval  19084  efgtval  19113  iscmn  19178  iscmnd  19183  submcmn2  19224  iscyg  19263  cycsubmcmn  19273  issrg  19522  isring  19566  ringidss  19595  prdsmgp  19628  mulgass3  19655  dvdsrval  19663  isirred  19717  isdrngd  19792  isdrngrd  19793  subrg1  19810  subrgmcl  19812  subrgdvds  19814  subrguss  19815  subrginv  19816  subrgdv  19817  subrgunit  19818  subrgugrp  19819  abvfval  19854  isabvd  19856  issrngd  19897  islmod  19903  islmodd  19905  scaffval  19917  lmodpropd  19962  lssset  19970  islssd  19972  prdslmodd  20006  islmhm  20064  reslmhm  20089  reslmhm2  20090  reslmhm2b  20091  islbs  20113  rlmvneg  20245  rrgval  20325  isphl  20590  ipffval  20610  isphld  20616  phssipval  20619  phssip  20620  phlssphl  20621  ocvfval  20628  isobs  20682  frlmplusgval  20726  frlmsubgval  20727  frlmvscafval  20728  frlmip  20740  frlmipval  20741  frlmup1  20760  lsslindf  20792  isassa  20818  isassad  20826  assamulgscmlem2  20860  psrval  20874  resspsradd  20941  resspsrmul  20942  resspsrvsca  20943  mplmon2mul  21027  ply1coe  21217  lply1binomsc  21228  evl1expd  21261  evl1scvarpw  21279  mamufval  21284  matplusg2  21324  matvsca2  21325  matplusgcell  21330  matsubgcell  21331  matinvgcell  21332  matvscacell  21333  matmulcell  21342  mpomatmul  21343  mat1  21344  mattposm  21356  mat1dimmul  21373  dmatmul  21394  dmatcrng  21399  scmataddcl  21413  scmatsubcl  21414  scmatcrng  21418  smatvscl  21421  scmatghm  21430  scmatmhm  21431  mvmulfval  21439  ma1repveval  21468  mdetrlin  21499  mdetrsca  21500  mdetmul  21520  madurid  21541  minmar1cl  21548  smadiadetglem1  21568  smadiadetr  21572  matinv  21574  slesolinv  21577  slesolinvbi  21578  cramerimplem3  21582  cpmatacl  21613  mat2pmatghm  21627  decpmatmullem  21668  decpmatmul  21669  pmatcollpw1lem1  21671  pmatcollpw2lem  21674  pmatcollpwlem  21677  pmatcollpw3lem  21680  mply1topmatval  21701  mp2pm2mplem1  21703  mp2pm2mplem4  21706  mp2pm2mplem5  21707  mp2pm2mp  21708  chpmat1d  21733  chpscmatgsummon  21742  chfacfpmmulgsum2  21762  xkocnv  22711  submtmd  23001  prdsdsf  23265  ressprdsds  23269  blfvalps  23281  prdsxmslem2  23427  tmsxpsval  23436  ngpds  23502  sgrimval  23530  subgngp  23533  tngngp  23552  tngngp3  23554  isnlm  23573  lssnlm  23599  isphtpy  23878  isphtpc  23891  pi1cpbl  23941  pi1addf  23944  pi1addval  23945  pi1grplem  23946  clmsub  23977  clmvsass  23986  clmvsdir  23988  isclmp  23994  cvsdiv  24029  iscph  24067  cphdir  24102  cphdi  24103  cph2di  24104  cph2subdi  24107  cphass  24108  tcphval  24115  ipcau2  24131  tcphcphlem1  24132  tcphcphlem2  24133  cphsscph  24148  caufval  24172  rrxip  24287  rrxvsca  24291  rrxplusgvscavalb  24292  rrxdsfival  24310  ehleudisval  24316  dvlip2  24892  q1pval  25051  r1pval  25054  dvntaylp  25263  efabl  25439  efsubm  25440  dchrmul  26129  istrkgc  26545  istrkgb  26546  istrkgcb  26547  istrkge  26548  istrkgl  26549  istrkgld  26550  iscgrg  26603  isismt  26625  tglngval  26642  legval  26675  ishlg  26693  mirval  26746  israg  26788  ishpg  26850  lmif  26876  islmib  26878  isinag  26929  ttgval  26966  wksonproplem  27792  wspthsnon  27936  iswwlksnon  27937  iswspthsnon  27940  isconngr  28272  isconngr1  28273  grpodivval  28616  dipfval  28783  ipval  28784  sspgval  28810  sspsval  28812  lnoval  28833  ajfval  28890  dipdir  28923  dipass  28926  htth  28999  isomnd  31046  submomnd  31055  inftmrel  31153  isinftm  31154  isslmd  31174  rngurd  31201  rdivmuldivd  31207  isorng  31217  suborng  31233  resv1r  31255  lsmidllsp  31302  idlinsubrg  31322  prmidlval  31326  idlsrgval  31362  idlsrg0g  31365  rprmval  31378  ply1chr  31383  drgextlsp  31395  fedgmullem1  31424  fedgmullem2  31425  fedgmul  31426  extdg1id  31452  smatlem  31461  submatminr1  31474  metidval  31554  pstmval  31559  pstmfval  31560  zlm0  31624  zlm1  31625  sitmval  32028  breprexp  32325  istrkg2d  32358  afsval  32363  mclsrcl  33236  mppsval  33247  bj-endval  35220  matunitlindflem2  35511  istotbnd  35664  isbnd  35675  rrnequiv  35730  isrngo  35792  rngohomval  35859  idlval  35908  pridlval  35928  lflset  36810  islfld  36813  ldualvadd  36880  ldualsmul  36886  ldualvs  36888  isopos  36931  cmtfvalN  36961  iscvlat  37074  ishlat1  37103  lineset  37489  psubspset  37495  paddfval  37548  paddval  37549  ltrnfset  37868  trnfsetN  37906  trlfset  37911  tgrpov  38499  erngplus  38554  erngmul  38557  erngplus-rN  38562  erngmul-rN  38565  erngdvlem3  38741  erngdvlem4  38742  erng0g  38745  erngdvlem3-rN  38749  erngdvlem4-rN  38750  dvaplusg  38760  dvamulr  38763  dvavadd  38766  dvavsca  38768  dvalveclem  38776  dvhmulr  38837  dvhfvadd  38842  dvhvadd  38843  dvhopvadd2  38845  dvhvaddcl  38846  dvhvaddcomN  38847  dvhvsca  38852  dvhlveclem  38859  dvh0g  38862  djavalN  38886  diblsmopel  38922  dicvaddcl  38941  cdlemn6  38953  dihffval  38981  dihopelvalcpre  38999  djhval  39149  lcdvaddval  39349  lcdsmul  39353  lcdvsval  39355  lcdlkreq2N  39374  hvmapffval  39509  hvmapfval  39510  hdmap1fval  39547  hgmapffval  39636  hgmapfval  39637  hgmapadd  39645  hlhilipval  39700  hlhilhillem  39711  mhphf  39995  prjspval  40150  prjspner1  40171  mnringvald  41504  ioorrnopnlem  43520  hoidmvval0b  43803  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvle  43813  ovnhoi  43816  hoiqssbl  43838  hspmbllem2  43840  vonioo  43895  vonicc  43898  ismgmd  45003  ismgmhm  45010  issubmgm  45016  resmgmhm  45025  resmgmhm2  45026  resmgmhm2b  45027  idfusubc  45097  rnghmval  45122  lidlmsgrp  45157  lidlrng  45158  zlidlring  45159  uzlidlring  45160  rnghmresel  45195  rngchom  45198  rngcco  45202  rnghmsubcsetclem1  45206  rhmresel  45241  ringchom  45244  ringcco  45248  rhmsubcsetclem1  45252  rhmsubcrngclem1  45258  irinitoringc  45300  ovmpordxf  45347  lincop  45422  lincval  45423  lincsum  45443  lincscm  45444  lmod1lem2  45502  lmod1lem3  45503  lmod1lem4  45504  ldepsnlinc  45522  lines  45750  line  45751  rrxlines  45752  rrxline  45753  spheres  45765  fvconstr  45856  fvconstrn0  45857  fvconstr2  45858  catprs  45965  thincmod  45985  isthincd2lem2  45990  isthincd  45991  mndtcco2  46044  mndtccatid  46045  grptcmon  46048  grptcepi  46049