Theorem oveqd 6667

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

Syntax hints:   → wi 4   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  oveq123d  6671  oveqdr  6674  csbov  6688  csbov12g  6689  ovmpt2dxf  6786  oprssov  6803  2mpt20  6882  ofeq  6899  mptmpt2opabbrd  7248  mptmpt2opabovd  7249  el2mpt2csbcl  7250  fnmpt2ovd  7252  ruclem1  14960  vdwapval  15677  vdwapid1  15679  vdwmc2  15683  vdwpc  15684  vdwlem5  15689  vdwlem8  15692  vdwlem13  15697  prdsval  16115  prdsdsval2  16144  pwsplusgval  16150  pwsmulrval  16151  pwsvscafval  16154  imasval  16171  iscat  16333  iscatd  16334  catidex  16335  catideu  16336  cidfval  16337  cidval  16338  catidd  16341  iscatd2  16342  catlid  16344  catrid  16345  homffval  16350  homfeqd  16355  homfeqval  16357  comfffval  16358  comffval  16359  comfeq  16366  comfeqd  16367  comfeqval  16368  catpropd  16369  oppcval  16373  oppcco  16377  monfval  16392  ismon  16393  oppcmon  16398  oppcepi  16399  sectffval  16410  sectfval  16411  invffval  16418  isoval  16425  dfiso2  16432  isofn  16435  invisoinvl  16450  invcoisoid  16452  isocoinvid  16453  issubc  16495  issubc3  16509  isfunc  16524  cofuval  16542  cofuval2  16547  funcres  16556  funcres2b  16557  funcres2  16558  funcres2c  16561  isfull  16570  isfth  16574  fullres2c  16599  natfval  16606  isnat  16607  fucval  16618  fucco  16622  fucpropd  16637  initoval  16647  termoval  16648  homarcl  16678  coafval  16714  resssetc  16742  resscatc  16755  catciso  16757  xpcval  16817  1stfval  16831  2ndfval  16834  prfval  16839  prfcl  16843  evlfval  16857  curfval  16863  curf1cl  16868  curfcl  16872  uncf1  16876  uncf2  16877  diag12  16884  diag2  16885  curf2ndf  16887  hofval  16892  hof1  16894  hof2fval  16895  hofcl  16899  yon12  16905  yon2  16906  hofpropd  16907  joinval  17005  meetval  17019  isdlat  17193  plusffval  17247  issstrmgm  17252  grpidval  17260  grpidd  17268  gsumvalx  17270  gsumpropd  17272  gsumress  17276  ismndd  17313  issubmnd  17318  submnd0  17320  ismhm  17337  issubm  17347  resmhm  17359  resmhm2  17360  resmhm2b  17361  isgrp  17428  isgrpd2e  17441  grpidd2  17459  grpinvfval  17460  imasgrp2  17530  imasgrp  17531  subg0  17600  subginv  17601  subgcl  17604  issubgrpd2  17610  isnsg  17623  isghm  17660  resghm  17676  isga  17724  subgga  17733  gasubg  17735  cntzfval  17753  resscntz  17764  odfval  17952  gexval  17993  lsmfval  18053  lsmvalx  18054  oppglsm  18057  subglsm  18086  pj1fval  18107  efgtval  18136  iscmn  18200  iscmnd  18205  submcmn2  18244  iscyg  18281  issrg  18507  isring  18551  ringidss  18577  prdsmgp  18610  mulgass3  18637  dvdsrval  18645  isirred  18699  isdrngd  18772  isdrngrd  18773  subrg1  18790  subrgmcl  18792  subrgdvds  18794  subrguss  18795  subrginv  18796  subrgdv  18797  subrgunit  18798  subrgugrp  18799  abvfval  18818  isabvd  18820  issrngd  18861  islmod  18867  islmodd  18869  scaffval  18881  lmodpropd  18926  lssset  18934  islssd  18936  prdslmodd  18969  islmhm  19027  reslmhm  19052  reslmhm2  19053  reslmhm2b  19054  islbs  19076  rlmvneg  19207  rrgval  19287  isassa  19315  isassad  19323  assamulgscmlem2  19349  psrval  19362  resspsradd  19416  resspsrmul  19417  resspsrvsca  19418  mplmon2mul  19501  ply1coe  19666  lply1binomsc  19677  evl1expd  19709  evl1scvarpw  19727  isphl  19973  ipffval  19993  isphld  19999  phssipval  20002  phssip  20003  ocvfval  20010  isobs  20064  frlmplusgval  20107  frlmsubgval  20108  frlmvscafval  20109  frlmip  20117  frlmipval  20118  frlmup1  20137  lsslindf  20169  mamufval  20191  matplusg2  20233  matvsca2  20234  matplusgcell  20239  matsubgcell  20240  matinvgcell  20241  matvscacell  20242  matmulcell  20251  mpt2matmul  20252  mat1  20253  mattposm  20265  mat1dimmul  20282  dmatmul  20303  dmatcrng  20308  scmataddcl  20322  scmatsubcl  20323  scmatcrng  20327  smatvscl  20330  scmatghm  20339  scmatmhm  20340  mvmulfval  20348  ma1repveval  20377  mdetrlin  20408  mdetrsca  20409  mdetmul  20429  madurid  20450  minmar1cl  20457  smadiadetglem1  20477  smadiadetr  20481  matinv  20483  slesolinv  20486  slesolinvbi  20487  cramerimplem3  20491  cpmatacl  20521  mat2pmatghm  20535  decpmatmullem  20576  decpmatmul  20577  pmatcollpw1lem1  20579  pmatcollpw2lem  20582  pmatcollpwlem  20585  pmatcollpw3lem  20588  mply1topmatval  20609  mp2pm2mplem1  20611  mp2pm2mplem4  20614  mp2pm2mplem5  20615  mp2pm2mp  20616  chpmat1d  20641  chpscmatgsummon  20650  chfacfpmmulgsum2  20670  xkocnv  21617  submtmd  21908  prdsdsf  22172  ressprdsds  22176  blfvalps  22188  prdsxmslem2  22334  tmsxpsval  22343  ngpds  22408  sgrimval  22436  subgngp  22439  tngngp  22458  tngngp3  22460  isnlm  22479  lssnlm  22505  isphtpy  22780  isphtpc  22793  pi1cpbl  22844  pi1addf  22847  pi1addval  22848  pi1grplem  22849  clmsub  22880  clmvsass  22889  clmvsdir  22891  isclmp  22897  cvsi  22930  cvsdiv  22932  iscph  22970  cphdir  23005  cphdi  23006  cph2di  23007  cph2subdi  23010  cphass  23011  tchval  23017  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  caufval  23073  rrxip  23178  dvlip2  23758  q1pval  23913  r1pval  23916  dvntaylp  24125  efabl  24296  efsubm  24297  dchrmul  24973  istrkgc  25353  istrkgb  25354  istrkgcb  25355  istrkge  25356  istrkgl  25357  istrkgld  25358  iscgrg  25407  isismt  25429  tglngval  25446  legval  25479  ishlg  25497  mirval  25550  israg  25592  ishpg  25651  lmif  25677  islmib  25679  isinag  25729  ttgval  25755  wksonproplem  26601  wspthsnon  26739  iswwlksnon  26740  iswspthsnon  26741  wwlks2onv  26847  isconngr  27049  isconngr1  27050  grpodivval  27389  dipfval  27557  ipval  27558  sspgval  27584  sspsval  27586  lnoval  27607  ajfval  27664  dipdir  27697  dipass  27700  htth  27775  isomnd  29701  submomnd  29710  inftmrel  29734  isinftm  29735  isslmd  29755  rngurd  29788  rdivmuldivd  29791  isorng  29799  suborng  29815  resv1r  29837  smatlem  29863  submatminr1  29876  metidval  29933  pstmval  29938  pstmfval  29939  zlm0  30006  zlm1  30007  sitmval  30411  breprexp  30711  istrkg2d  30744  afsval  30749  mclsrcl  31458  mppsval  31469  matunitlindflem2  33406  istotbnd  33568  isbnd  33579  rrnequiv  33634  isrngo  33696  rngohomval  33763  idlval  33812  pridlval  33832  lflset  34346  islfld  34349  ldualvadd  34416  ldualsmul  34422  ldualvs  34424  isopos  34467  cmtfvalN  34497  iscvlat  34610  ishlat1  34639  lineset  35024  psubspset  35030  paddfval  35083  paddval  35084  ltrnfset  35403  trnfsetN  35442  trlfset  35447  tgrpov  36036  erngplus  36091  erngmul  36094  erngplus-rN  36099  erngmul-rN  36102  erngdvlem3  36278  erngdvlem4  36279  erng0g  36282  erngdvlem3-rN  36286  erngdvlem4-rN  36287  dvaplusg  36297  dvamulr  36300  dvavadd  36303  dvavsca  36305  dvalveclem  36314  dvhmulr  36375  dvhfvadd  36380  dvhvadd  36381  dvhopvadd2  36383  dvhvaddcl  36384  dvhvaddcomN  36385  dvhvsca  36390  dvhlveclem  36397  dvh0g  36400  djavalN  36424  diblsmopel  36460  dicvaddcl  36479  cdlemn6  36491  dihffval  36519  dihopelvalcpre  36537  djhval  36687  lcdvaddval  36887  lcdsmul  36891  lcdvsval  36893  lcdlkreq2N  36912  hvmapffval  37047  hvmapfval  37048  hdmap1fval  37086  hgmapffval  37177  hgmapfval  37178  hgmapadd  37186  hlhilipval  37241  hlhilhillem  37252  ioorrnopnlem  40524  hoidmvval0b  40804  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvle  40814  ovnhoi  40817  hoiqssbl  40839  hspmbllem2  40841  vonioo  40896  vonicc  40899  ismgmd  41776  ismgmhm  41783  issubmgm  41789  resmgmhm  41798  resmgmhm2  41799  resmgmhm2b  41800  idfusubc  41866  rnghmval  41891  lidlmsgrp  41926  lidlrng  41927  zlidlring  41928  uzlidlring  41929  rnghmresel  41964  rngchom  41967  rngcco  41971  rnghmsubcsetclem1  41975  rhmresel  42010  ringchom  42013  ringcco  42017  rhmsubcsetclem1  42021  rhmsubcrngclem1  42027  irinitoringc  42069  ovmpt2rdxf  42117  lincop  42197  lincval  42198  lincsum  42218  lincscm  42219  lmod1lem2  42277  lmod1lem3  42278  lmod1lem4  42279  ldepsnlinc  42297