Theorem oveqd 6322

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

Hypothesis

Ref	Expression
oveq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
oveqd	|- ( ph -> ( C A D ) = ( C B D ) )

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq 6311	. 2 |- ( A = B -> ( C A D ) = ( C B D ) )
3	1, 2	syl 17	1 |- ( ph -> ( C A D ) = ( C B D ) )

Syntax hints:   -> wi 4   = wceq 1437  (class class class)co 6305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308

This theorem is referenced by:  oveq123d  6326  oveqdr  6329  csbov  6340  csbov12g  6341  ovmpt2dxf  6436  oprssov  6452  ofeq  6547  fnmpt2ovd  6885  ruclem1  14261  vdwapval  14877  vdwapid1  14879  vdwmc2  14883  vdwpc  14884  vdwlem5  14889  vdwlem8  14892  vdwlem13  14897  prdsval  15303  prdsdsval2  15332  pwsplusgval  15338  pwsmulrval  15339  pwsvscafval  15342  imasval  15359  iscat  15520  iscatd  15521  catidex  15522  catideu  15523  cidfval  15524  cidval  15525  catidd  15528  iscatd2  15529  catlid  15531  catrid  15532  homffval  15537  homfeqd  15542  homfeqval  15544  comfffval  15545  comffval  15546  comfeq  15553  comfeqd  15554  comfeqval  15555  catpropd  15556  oppcval  15560  oppcco  15564  monfval  15579  ismon  15580  oppcmon  15585  oppcepi  15586  sectffval  15597  sectfval  15598  invffval  15605  isoval  15612  dfiso2  15619  isofn  15622  invisoinvl  15637  invcoisoid  15639  isocoinvid  15640  issubc  15682  issubc3  15696  isfunc  15711  cofuval  15729  cofuval2  15734  funcres  15743  funcres2b  15744  funcres2  15745  funcres2c  15748  isfull  15757  isfth  15761  fullres2c  15786  natfval  15793  isnat  15794  fucval  15805  fucco  15809  fucpropd  15824  initoval  15834  termoval  15835  homarcl  15865  coafval  15901  resssetc  15929  resscatc  15942  catciso  15944  xpcval  16004  1stfval  16018  2ndfval  16021  prfval  16026  prfcl  16030  evlfval  16044  curfval  16050  curf1cl  16055  curfcl  16059  uncf1  16063  uncf2  16064  diag12  16071  diag2  16072  curf2ndf  16074  hofval  16079  hof1  16081  hof2fval  16082  hofcl  16086  yon12  16092  yon2  16093  hofpropd  16094  joinval  16193  meetval  16207  isdlat  16381  plusffval  16435  grpidval  16445  grpidd  16453  gsumvalx  16455  gsumpropd  16457  gsumress  16461  ismndOLD  16484  ismndd  16501  issubmnd  16506  submnd0  16508  ismhm  16526  issubm  16536  resmhm  16548  resmhm2  16549  resmhm2b  16550  isgrp  16619  isgrpd2e  16630  grpidd2  16645  grpinvfval  16646  imasgrp2  16743  imasgrp  16744  subg0  16765  subginv  16766  subgcl  16769  issubgrpd2  16775  isnsg  16788  isghm  16825  resghm  16841  isga  16887  subgga  16896  gasubg  16898  cntzfval  16916  resscntz  16927  odfval  17115  gexval  17156  lsmfval  17216  lsmvalx  17217  oppglsm  17220  subglsm  17249  pj1fval  17270  efgtval  17299  iscmn  17363  iscmnd  17368  submcmn2  17405  iscyg  17440  issrg  17667  isring  17710  ringidss  17733  prdsmgp  17764  mulgass3  17791  dvdsrval  17799  isirred  17853  isdrngd  17926  isdrngrd  17927  subrg1  17944  subrgmcl  17946  subrgdvds  17948  subrguss  17949  subrginv  17950  subrgdv  17951  subrgunit  17952  subrgugrp  17953  abvfval  17972  isabvd  17974  issrngd  18015  islmod  18021  islmodd  18023  scaffval  18035  lmodpropd  18077  lssset  18083  islssd  18085  prdslmodd  18118  islmhm  18176  reslmhm  18201  reslmhm2  18202  reslmhm2b  18203  islbs  18225  rlmvneg  18356  rrgval  18437  isassa  18465  isassad  18473  assamulgscmlem2  18499  psrval  18512  resspsradd  18566  resspsrmul  18567  resspsrvsca  18568  mplmon2mul  18650  ply1coe  18815  ply1coeOLD  18816  lply1binomsc  18827  evl1expd  18859  evl1scvarpw  18877  isphl  19117  ipffval  19137  isphld  19143  ocvfval  19151  isobs  19205  frlmplusgval  19248  frlmsubgval  19249  frlmvscafval  19250  frlmip  19258  frlmipval  19259  frlmup1  19278  lsslindf  19310  mamufval  19332  matplusg2  19374  matvsca2  19375  matplusgcell  19380  matsubgcell  19381  matinvgcell  19382  matvscacell  19383  matmulcell  19392  mpt2matmul  19393  mat1  19394  mattposm  19406  mat1dimmul  19423  dmatmul  19444  dmatcrng  19449  scmataddcl  19463  scmatsubcl  19464  scmatcrng  19468  smatvscl  19471  scmatghm  19480  scmatmhm  19481  mvmulfval  19489  ma1repveval  19518  mdetrlin  19549  mdetrsca  19550  mdetmul  19570  madurid  19591  minmar1cl  19598  smadiadetglem1  19618  smadiadetr  19622  matinv  19624  slesolinv  19627  slesolinvbi  19628  cramerimplem3  19632  cpmatacl  19662  mat2pmatghm  19676  decpmatmullem  19717  decpmatmul  19718  pmatcollpw1lem1  19720  pmatcollpw2lem  19723  pmatcollpwlem  19726  pmatcollpw3lem  19729  mply1topmatval  19750  mp2pm2mplem1  19752  mp2pm2mplem4  19755  mp2pm2mplem5  19756  mp2pm2mp  19757  chpmat1d  19782  chpscmatgsummon  19791  chfacfpmmulgsum2  19811  xkocnv  20751  submtmd  21041  prdsdsf  21304  ressprdsds  21308  blfvalps  21320  prdsxmslem2  21466  tmsxpsval  21475  ngpds  21539  subgngp  21565  tngngp  21584  isnlm  21600  lssnlm  21625  isphtpy  21896  isphtpc  21909  pi1cpbl  21959  pi1addf  21962  pi1addval  21963  pi1grplem  21964  clmsub  21995  clmvsass  22002  clmvsdir  22003  cvsdiv  22024  iscph  22032  cphdir  22066  cphdi  22067  cph2di  22068  cph2subdi  22071  cphass  22072  tchval  22076  ipcau2  22092  tchcphlem1  22093  tchcphlem2  22094  caufval  22129  rrxip  22233  dvlip2  22815  q1pval  22970  r1pval  22973  dvntaylp  23182  efabl  23355  efsubm  23356  dchrmul  24030  istrkgc  24356  istrkgb  24357  istrkgcb  24358  istrkge  24359  istrkgl  24360  istrkgld  24361  iscgrg  24411  isismt  24430  tglngval  24447  legval  24480  ishlg  24498  mirval  24551  israg  24590  ishpg  24648  lmif  24674  islmib  24676  isinag  24723  ttgval  24742  wlkon  25097  trlon  25106  trlonprop  25108  pthon  25141  pthonprop  25143  spthon  25148  spthonprp  25151  isconngra  25236  isconngra1  25237  is2wlkonot  25427  is2spthonot  25428  2wlkonot  25429  2spthonot  25430  2wlksot  25431  2spthsot  25432  2wlkonot3v  25439  2spthonot3v  25440  grpodivval  25807  gxval  25822  subgoov  25869  isrngo  25942  vcoprne  26034  dipfval  26174  ipval  26175  sspgval  26204  sspsval  26206  lnoval  26229  ajfval  26286  dipdir  26319  dipass  26322  htth  26397  isomnd  28293  submomnd  28302  inftmrel  28326  isinftm  28327  isslmd  28347  rngurd  28381  rdivmuldivd  28384  isorng  28392  suborng  28408  resv1r  28430  smatlem  28453  submatminr1  28466  metidval  28523  pstmval  28528  pstmfval  28529  zlm0  28596  zlm1  28597  sitmval  29001  istrkg2d  29262  afsval  29267  mclsrcl  29978  mppsval  29989  istotbnd  31795  isbnd  31806  rrnequiv  31861  rngohomval  31897  idlval  31940  pridlval  31960  lflset  32324  islfld  32327  ldualvadd  32394  ldualsmul  32400  ldualvs  32402  isopos  32445  cmtfvalN  32475  iscvlat  32588  ishlat1  32617  lineset  33002  psubspset  33008  paddfval  33061  paddval  33062  ltrnfset  33381  trnfsetN  33420  trlfset  33425  tgrpov  34014  erngplus  34069  erngmul  34072  erngplus-rN  34077  erngmul-rN  34080  erngdvlem3  34256  erngdvlem4  34257  erng0g  34260  erngdvlem3-rN  34264  erngdvlem4-rN  34265  dvaplusg  34275  dvamulr  34278  dvavadd  34281  dvavsca  34283  dvalveclem  34292  dvhmulr  34353  dvhfvadd  34358  dvhvadd  34359  dvhopvadd2  34361  dvhvaddcl  34362  dvhvaddcomN  34363  dvhvsca  34368  dvhlveclem  34375  dvh0g  34378  djavalN  34402  diblsmopel  34438  dicvaddcl  34457  cdlemn6  34469  dihffval  34497  dihopelvalcpre  34515  djhval  34665  lcdvaddval  34865  lcdsmul  34869  lcdvsval  34871  lcdlkreq2N  34890  hvmapffval  35025  hvmapfval  35026  hdmap1fval  35064  hgmapffval  35155  hgmapfval  35156  hgmapadd  35164  hlhilipval  35219  hlhilhillem  35230  ismgmd  38524  ismgmhm  38531  issubmgm  38537  resmgmhm  38546  resmgmhm2  38547  resmgmhm2b  38548  idfusubc  38614  rnghmval  38639  lidlmsgrp  38674  lidlrng  38675  zlidlring  38676  uzlidlring  38677  rnghmresel  38714  rngchom  38717  rngcco  38721  rnghmsubcsetclem1  38725  rhmresel  38760  ringchom  38763  ringcco  38767  rhmsubcsetclem1  38771  rhmsubcrngclem1  38777  irinitoringc  38819  ovmpt2rdxf  38870  lincop  38951  lincval  38952  lincsum  38972  lincscm  38973  lmod1lem2  39031  lmod1lem3  39032  lmod1lem4  39033  ldepsnlinc  39051