Theorem oveqd 6566

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

Syntax hints:   → wi 4   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  oveq123d  6570  oveqdr  6573  csbov  6586  csbov12g  6587  ovmpt2dxf  6684  oprssov  6701  2mpt20  6780  ofeq  6797  el2mpt2csbcl  7137  fnmpt2ovd  7139  ruclem1  14799  vdwapval  15515  vdwapid1  15517  vdwmc2  15521  vdwpc  15522  vdwlem5  15527  vdwlem8  15530  vdwlem13  15535  prdsval  15938  prdsdsval2  15967  pwsplusgval  15973  pwsmulrval  15974  pwsvscafval  15977  imasval  15994  iscat  16156  iscatd  16157  catidex  16158  catideu  16159  cidfval  16160  cidval  16161  catidd  16164  iscatd2  16165  catlid  16167  catrid  16168  homffval  16173  homfeqd  16178  homfeqval  16180  comfffval  16181  comffval  16182  comfeq  16189  comfeqd  16190  comfeqval  16191  catpropd  16192  oppcval  16196  oppcco  16200  monfval  16215  ismon  16216  oppcmon  16221  oppcepi  16222  sectffval  16233  sectfval  16234  invffval  16241  isoval  16248  dfiso2  16255  isofn  16258  invisoinvl  16273  invcoisoid  16275  isocoinvid  16276  issubc  16318  issubc3  16332  isfunc  16347  cofuval  16365  cofuval2  16370  funcres  16379  funcres2b  16380  funcres2  16381  funcres2c  16384  isfull  16393  isfth  16397  fullres2c  16422  natfval  16429  isnat  16430  fucval  16441  fucco  16445  fucpropd  16460  initoval  16470  termoval  16471  homarcl  16501  coafval  16537  resssetc  16565  resscatc  16578  catciso  16580  xpcval  16640  1stfval  16654  2ndfval  16657  prfval  16662  prfcl  16666  evlfval  16680  curfval  16686  curf1cl  16691  curfcl  16695  uncf1  16699  uncf2  16700  diag12  16707  diag2  16708  curf2ndf  16710  hofval  16715  hof1  16717  hof2fval  16718  hofcl  16722  yon12  16728  yon2  16729  hofpropd  16730  joinval  16828  meetval  16842  isdlat  17016  plusffval  17070  issstrmgm  17075  grpidval  17083  grpidd  17091  gsumvalx  17093  gsumpropd  17095  gsumress  17099  ismndd  17136  issubmnd  17141  submnd0  17143  ismhm  17160  issubm  17170  resmhm  17182  resmhm2  17183  resmhm2b  17184  isgrp  17251  isgrpd2e  17264  grpidd2  17282  grpinvfval  17283  imasgrp2  17353  imasgrp  17354  subg0  17423  subginv  17424  subgcl  17427  issubgrpd2  17433  isnsg  17446  isghm  17483  resghm  17499  isga  17547  subgga  17556  gasubg  17558  cntzfval  17576  resscntz  17587  odfval  17775  gexval  17816  lsmfval  17876  lsmvalx  17877  oppglsm  17880  subglsm  17909  pj1fval  17930  efgtval  17959  iscmn  18023  iscmnd  18028  submcmn2  18067  iscyg  18104  issrg  18330  isring  18374  ringidss  18400  prdsmgp  18433  mulgass3  18460  dvdsrval  18468  isirred  18522  isdrngd  18595  isdrngrd  18596  subrg1  18613  subrgmcl  18615  subrgdvds  18617  subrguss  18618  subrginv  18619  subrgdv  18620  subrgunit  18621  subrgugrp  18622  abvfval  18641  isabvd  18643  issrngd  18684  islmod  18690  islmodd  18692  scaffval  18704  lmodpropd  18749  lssset  18755  islssd  18757  prdslmodd  18790  islmhm  18848  reslmhm  18873  reslmhm2  18874  reslmhm2b  18875  islbs  18897  rlmvneg  19028  rrgval  19108  isassa  19136  isassad  19144  assamulgscmlem2  19170  psrval  19183  resspsradd  19237  resspsrmul  19238  resspsrvsca  19239  mplmon2mul  19322  ply1coe  19487  lply1binomsc  19498  evl1expd  19530  evl1scvarpw  19548  isphl  19792  ipffval  19812  isphld  19818  phssipval  19821  phssip  19822  ocvfval  19829  isobs  19883  frlmplusgval  19926  frlmsubgval  19927  frlmvscafval  19928  frlmip  19936  frlmipval  19937  frlmup1  19956  lsslindf  19988  mamufval  20010  matplusg2  20052  matvsca2  20053  matplusgcell  20058  matsubgcell  20059  matinvgcell  20060  matvscacell  20061  matmulcell  20070  mpt2matmul  20071  mat1  20072  mattposm  20084  mat1dimmul  20101  dmatmul  20122  dmatcrng  20127  scmataddcl  20141  scmatsubcl  20142  scmatcrng  20146  smatvscl  20149  scmatghm  20158  scmatmhm  20159  mvmulfval  20167  ma1repveval  20196  mdetrlin  20227  mdetrsca  20228  mdetmul  20248  madurid  20269  minmar1cl  20276  smadiadetglem1  20296  smadiadetr  20300  matinv  20302  slesolinv  20305  slesolinvbi  20306  cramerimplem3  20310  cpmatacl  20340  mat2pmatghm  20354  decpmatmullem  20395  decpmatmul  20396  pmatcollpw1lem1  20398  pmatcollpw2lem  20401  pmatcollpwlem  20404  pmatcollpw3lem  20407  mply1topmatval  20428  mp2pm2mplem1  20430  mp2pm2mplem4  20433  mp2pm2mplem5  20434  mp2pm2mp  20435  chpmat1d  20460  chpscmatgsummon  20469  chfacfpmmulgsum2  20489  xkocnv  21427  submtmd  21718  prdsdsf  21982  ressprdsds  21986  blfvalps  21998  prdsxmslem2  22144  tmsxpsval  22153  ngpds  22218  sgrimval  22246  subgngp  22249  tngngp  22268  tngngp3  22270  isnlm  22289  lssnlm  22315  isphtpy  22588  isphtpc  22601  pi1cpbl  22652  pi1addf  22655  pi1addval  22656  pi1grplem  22657  clmsub  22688  clmvsass  22697  clmvsdir  22699  isclmp  22705  cvsi  22738  cvsdiv  22740  iscph  22778  cphdir  22813  cphdi  22814  cph2di  22815  cph2subdi  22818  cphass  22819  tchval  22825  ipcau2  22841  tchcphlem1  22842  tchcphlem2  22843  caufval  22881  rrxip  22986  dvlip2  23562  q1pval  23717  r1pval  23720  dvntaylp  23929  efabl  24100  efsubm  24101  dchrmul  24773  istrkgc  25153  istrkgb  25154  istrkgcb  25155  istrkge  25156  istrkgl  25157  istrkgld  25158  iscgrg  25207  isismt  25229  tglngval  25246  legval  25279  ishlg  25297  mirval  25350  israg  25392  ishpg  25451  lmif  25477  islmib  25479  isinag  25529  ttgval  25555  wlkon  26061  trlon  26070  trlonprop  26072  pthon  26105  pthonprop  26107  spthon  26112  spthonprp  26115  isconngra  26200  isconngra1  26201  is2wlkonot  26390  is2spthonot  26391  2wlkonot  26392  2spthonot  26393  2wlksot  26394  2spthsot  26395  2wlkonot3v  26402  2spthonot3v  26403  grpodivval  26773  dipfval  26941  ipval  26942  sspgval  26968  sspsval  26970  lnoval  26991  ajfval  27048  dipdir  27081  dipass  27084  htth  27159  isomnd  29032  submomnd  29041  inftmrel  29065  isinftm  29066  isslmd  29086  rngurd  29119  rdivmuldivd  29122  isorng  29130  suborng  29146  resv1r  29168  smatlem  29191  submatminr1  29204  metidval  29261  pstmval  29266  pstmfval  29267  zlm0  29334  zlm1  29335  sitmval  29738  istrkg2d  29997  afsval  30002  mclsrcl  30712  mppsval  30723  matunitlindflem2  32576  istotbnd  32738  isbnd  32749  rrnequiv  32804  isrngo  32866  rngohomval  32933  idlval  32982  pridlval  33002  lflset  33364  islfld  33367  ldualvadd  33434  ldualsmul  33440  ldualvs  33442  isopos  33485  cmtfvalN  33515  iscvlat  33628  ishlat1  33657  lineset  34042  psubspset  34048  paddfval  34101  paddval  34102  ltrnfset  34421  trnfsetN  34460  trlfset  34465  tgrpov  35054  erngplus  35109  erngmul  35112  erngplus-rN  35117  erngmul-rN  35120  erngdvlem3  35296  erngdvlem4  35297  erng0g  35300  erngdvlem3-rN  35304  erngdvlem4-rN  35305  dvaplusg  35315  dvamulr  35318  dvavadd  35321  dvavsca  35323  dvalveclem  35332  dvhmulr  35393  dvhfvadd  35398  dvhvadd  35399  dvhopvadd2  35401  dvhvaddcl  35402  dvhvaddcomN  35403  dvhvsca  35408  dvhlveclem  35415  dvh0g  35418  djavalN  35442  diblsmopel  35478  dicvaddcl  35497  cdlemn6  35509  dihffval  35537  dihopelvalcpre  35555  djhval  35705  lcdvaddval  35905  lcdsmul  35909  lcdvsval  35911  lcdlkreq2N  35930  hvmapffval  36065  hvmapfval  36066  hdmap1fval  36104  hgmapffval  36195  hgmapfval  36196  hgmapadd  36204  hlhilipval  36259  hlhilhillem  36270  ioorrnopnlem  39200  hoidmvval0b  39480  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvle  39490  ovnhoi  39493  hoiqssbl  39515  hspmbllem2  39517  vonioo  39573  vonicc  39576  mptmpt2opabbrd  40335  mptmpt2opabovd  40336  1wlksonproplem  40912  wspthsnon  41050  iswwlksnon  41051  iswspthsnon  41052  wwlks2onv  41158  isconngr  41356  isconngr1  41357  ismgmd  41566  ismgmhm  41573  issubmgm  41579  resmgmhm  41588  resmgmhm2  41589  resmgmhm2b  41590  idfusubc  41656  rnghmval  41681  lidlmsgrp  41716  lidlrng  41717  zlidlring  41718  uzlidlring  41719  rnghmresel  41756  rngchom  41759  rngcco  41763  rnghmsubcsetclem1  41767  rhmresel  41802  ringchom  41805  ringcco  41809  rhmsubcsetclem1  41813  rhmsubcrngclem1  41819  irinitoringc  41861  ovmpt2rdxf  41910  lincop  41991  lincval  41992  lincsum  42012  lincscm  42013  lmod1lem2  42071  lmod1lem3  42072  lmod1lem4  42073  ldepsnlinc  42091