Theorem oveqd 6298

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 6287	. 2 |- ( A = B -> ( C A D ) = ( C B D ) )
3	1, 2	syl 16	1 |- ( ph -> ( C A D ) = ( C B D ) )

Syntax hints:   -> wi 4   = wceq 1383  (class class class)co 6281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284

This theorem is referenced by:  oveq123d  6302  oveqdr  6305  csbov  6316  csbov12g  6318  ovmpt2dxf  6413  oprssov  6429  ofeq  6527  fnmpt2ovd  6863  ruclem1  13841  vdwapval  14368  vdwapid1  14370  vdwmc2  14374  vdwpc  14375  vdwlem5  14380  vdwlem8  14383  vdwlem13  14388  prdsval  14729  prdsdsval2  14758  pwsplusgval  14764  pwsmulrval  14765  pwsvscafval  14768  imasval  14785  iscat  14946  iscatd  14947  catidex  14948  catideu  14949  cidfval  14950  cidval  14951  catidd  14954  iscatd2  14955  catlid  14957  catrid  14958  homffval  14963  homfeqd  14967  homfeqval  14969  comfffval  14970  comffval  14971  comfeq  14978  comfeqd  14979  comfeqval  14980  catpropd  14981  oppcval  14985  oppcco  14989  monfval  15004  ismon  15005  oppcmon  15010  oppcepi  15011  sectffval  15022  sectfval  15023  invffval  15029  isoval  15036  issubc  15081  issubc3  15092  isfunc  15107  cofuval  15125  cofuval2  15130  funcres  15139  funcres2b  15140  funcres2  15141  funcres2c  15144  isfull  15153  isfth  15157  fullres2c  15182  natfval  15189  isnat  15190  fucval  15201  fucco  15205  fucpropd  15220  homarcl  15229  coafval  15265  resssetc  15293  resscatc  15306  catciso  15308  xpcval  15320  1stfval  15334  2ndfval  15337  prfval  15342  prfcl  15346  evlfval  15360  curfval  15366  curf1cl  15371  curfcl  15375  uncf1  15379  uncf2  15380  diag12  15387  diag2  15388  curf2ndf  15390  hofval  15395  hof1  15397  hof2fval  15398  hofcl  15402  yon12  15408  yon2  15409  hofpropd  15410  joinval  15509  meetval  15523  isdlat  15697  plusffval  15751  grpidval  15761  grpidd  15769  gsumvalx  15771  gsumpropd  15773  gsumress  15777  ismndOLD  15800  ismndd  15817  issubmnd  15822  submnd0  15824  ismhm  15842  issubm  15852  resmhm  15864  resmhm2  15865  resmhm2b  15866  isgrp  15935  isgrpd2e  15946  grpidd2  15961  grpinvfval  15962  imasgrp2  16059  imasgrp  16060  subg0  16081  subginv  16082  subgcl  16085  issubgrpd2  16091  isnsg  16104  isghm  16141  resghm  16157  isga  16203  subgga  16212  gasubg  16214  cntzfval  16232  resscntz  16243  odfval  16431  gexval  16472  lsmfval  16532  lsmvalx  16533  oppglsm  16536  subglsm  16565  pj1fval  16586  efgtval  16615  iscmn  16679  iscmnd  16684  submcmn2  16721  iscyg  16756  issrg  17033  isring  17076  ringidss  17099  prdsmgp  17133  mulgass3  17160  dvdsrval  17168  isirred  17222  isdrngd  17295  isdrngrd  17296  subrg1  17313  subrgmcl  17315  subrgdvds  17317  subrguss  17318  subrginv  17319  subrgdv  17320  subrgunit  17321  subrgugrp  17322  abvfval  17341  isabvd  17343  issrngd  17384  islmod  17390  islmodd  17392  scaffval  17404  lmodpropd  17447  lssset  17454  islssd  17456  prdslmodd  17489  islmhm  17547  reslmhm  17572  reslmhm2  17573  reslmhm2b  17574  islbs  17596  rlmvneg  17727  rrgval  17809  isassa  17838  isassad  17846  assamulgscmlem2  17872  psrval  17885  resspsradd  17945  resspsrmul  17946  resspsrvsca  17947  mplmon2mul  18040  ply1coe  18211  ply1coeOLD  18212  lply1binomsc  18223  evl1expd  18255  evl1scvarpw  18273  isphl  18536  ipffval  18556  isphld  18562  ocvfval  18570  isobs  18624  frlmplusgval  18670  frlmsubgval  18671  frlmvscafval  18672  frlmip  18682  frlmipval  18683  frlmup1  18705  lsslindf  18738  mamufval  18760  matplusg2  18802  matvsca2  18803  matplusgcell  18808  matsubgcell  18809  matinvgcell  18810  matvscacell  18811  matmulcell  18820  mpt2matmul  18821  mat1  18822  mattposm  18834  mat1dimmul  18851  dmatmul  18872  dmatcrng  18877  scmataddcl  18891  scmatsubcl  18892  scmatcrng  18896  smatvscl  18899  scmatghm  18908  scmatmhm  18909  mvmulfval  18917  ma1repveval  18946  mdetrlin  18977  mdetrsca  18978  mdetmul  18998  madurid  19019  minmar1cl  19026  smadiadetglem1  19046  smadiadetr  19050  matinv  19052  slesolinv  19055  slesolinvbi  19056  cramerimplem3  19060  cpmatacl  19090  mat2pmatghm  19104  decpmatmullem  19145  decpmatmul  19146  pmatcollpw1lem1  19148  pmatcollpw2lem  19151  pmatcollpwlem  19154  pmatcollpw3lem  19157  mply1topmatval  19178  mp2pm2mplem1  19180  mp2pm2mplem4  19183  mp2pm2mplem5  19184  mp2pm2mp  19185  chpmat1d  19210  chpscmatgsummon  19219  chfacfpmmulgsum2  19239  xkocnv  20188  submtmd  20476  prdsdsf  20743  ressprdsds  20747  blfvalps  20759  prdsxmslem2  20905  tmsxpsval  20914  ngpds  20996  subgngp  21022  tngngp  21041  isnlm  21057  lssnlm  21082  isphtpy  21354  isphtpc  21367  pi1cpbl  21417  pi1addf  21420  pi1addval  21421  pi1grplem  21422  clmsub  21453  clmvsass  21460  clmvsdir  21461  cvsdiv  21482  iscph  21490  cphdir  21524  cphdi  21525  cph2di  21526  cph2subdi  21529  cphass  21530  tchval  21534  ipcau2  21550  tchcphlem1  21551  tchcphlem2  21552  caufval  21587  rrxip  21695  dvlip2  22269  q1pval  22427  r1pval  22430  dvntaylp  22638  efabl  22809  efsubm  22810  dchrmul  23395  istrkgc  23723  istrkgb  23724  istrkgcb  23725  istrkge  23726  istrkgl  23727  istrkg2d  23728  istrkgld  23729  iscgrg  23776  isismt  23793  tglngval  23810  legval  23843  mirval  23908  israg  23946  ishpg  24000  lmif  24023  islmib  24025  iscgra  24041  ttgval  24050  wlkon  24405  trlon  24414  trlonprop  24416  pthon  24449  pthonprop  24451  spthon  24456  spthonprp  24459  isconngra  24544  isconngra1  24545  is2wlkonot  24735  is2spthonot  24736  2wlkonot  24737  2spthonot  24738  2wlksot  24739  2spthsot  24740  2wlkonot3v  24747  2spthonot3v  24748  grpodivval  25117  gxval  25132  subgoov  25179  isrngo  25252  vcoprne  25344  dipfval  25484  ipval  25485  sspgval  25514  sspsval  25516  lnoval  25539  ajfval  25596  dipdir  25629  dipass  25632  htth  25707  isomnd  27564  submomnd  27573  inftmrel  27597  isinftm  27598  isslmd  27618  rngurd  27651  rdivmuldivd  27654  isorng  27662  suborng  27678  resv1r  27700  metidval  27742  pstmval  27747  pstmfval  27748  zlm0  27816  zlm1  27817  sitmval  28163  afsval  28424  mclsrcl  28794  mppsval  28805  istotbnd  30240  isbnd  30251  rrnequiv  30306  rngohomval  30342  idlval  30385  pridlval  30405  ismgmd  32302  ismgmhm  32309  issubmgm  32315  resmgmhm  32324  resmgmhm2  32325  resmgmhm2b  32326  idfusubc  32399  rnghmval  32415  lidlmsgrp  32442  lidlrng  32443  zlidlring  32444  uzlidlring  32445  rnghmresel  32512  rngchom  32515  rngcco  32519  rnghmsubcsetclem1  32523  rhmresel  32555  ringchom  32558  ringcco  32562  rhmsubcsetclem1  32566  rhmsubcrngclem1  32572  ovmpt2rdxf  32661  lincop  32744  lincval  32745  lincsum  32765  lincscm  32766  lmod1lem2  32824  lmod1lem3  32825  lmod1lem4  32826  ldepsnlinc  32844  lflset  34524  islfld  34527  ldualvadd  34594  ldualsmul  34600  ldualvs  34602  isopos  34645  cmtfvalN  34675  iscvlat  34788  ishlat1  34817  lineset  35202  psubspset  35208  paddfval  35261  paddval  35262  ltrnfset  35581  trnfsetN  35620  trlfset  35625  tgrpov  36214  erngplus  36269  erngmul  36272  erngplus-rN  36277  erngmul-rN  36280  erngdvlem3  36456  erngdvlem4  36457  erng0g  36460  erngdvlem3-rN  36464  erngdvlem4-rN  36465  dvaplusg  36475  dvamulr  36478  dvavadd  36481  dvavsca  36483  dvalveclem  36492  dvhmulr  36553  dvhfvadd  36558  dvhvadd  36559  dvhopvadd2  36561  dvhvaddcl  36562  dvhvaddcomN  36563  dvhvsca  36568  dvhlveclem  36575  dvh0g  36578  djavalN  36602  diblsmopel  36638  dicvaddcl  36657  cdlemn6  36669  dihffval  36697  dihopelvalcpre  36715  djhval  36865  lcdvaddval  37065  lcdsmul  37069  lcdvsval  37071  lcdlkreq2N  37090  hvmapffval  37225  hvmapfval  37226  hdmap1fval  37264  hgmapffval  37355  hgmapfval  37356  hgmapadd  37364  hlhilipval  37419  hlhilhillem  37430