Theorem oveqd 6213

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 6202	. 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 1399  (class class class)co 6196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199

This theorem is referenced by:  oveq123d  6217  oveqdr  6220  csbov  6231  csbov12g  6232  ovmpt2dxf  6327  oprssov  6343  ofeq  6441  fnmpt2ovd  6777  ruclem1  13966  vdwapval  14493  vdwapid1  14495  vdwmc2  14499  vdwpc  14500  vdwlem5  14505  vdwlem8  14508  vdwlem13  14513  prdsval  14862  prdsdsval2  14891  pwsplusgval  14897  pwsmulrval  14898  pwsvscafval  14901  imasval  14918  iscat  15079  iscatd  15080  catidex  15081  catideu  15082  cidfval  15083  cidval  15084  catidd  15087  iscatd2  15088  catlid  15090  catrid  15091  homffval  15096  homfeqd  15101  homfeqval  15103  comfffval  15104  comffval  15105  comfeq  15112  comfeqd  15113  comfeqval  15114  catpropd  15115  oppcval  15119  oppcco  15123  monfval  15138  ismon  15139  oppcmon  15144  oppcepi  15145  sectffval  15156  sectfval  15157  invffval  15164  isoval  15171  dfiso2  15178  isofn  15181  invisoinvl  15196  invcoisoid  15198  isocoinvid  15199  issubc  15241  issubc3  15255  isfunc  15270  cofuval  15288  cofuval2  15293  funcres  15302  funcres2b  15303  funcres2  15304  funcres2c  15307  isfull  15316  isfth  15320  fullres2c  15345  natfval  15352  isnat  15353  fucval  15364  fucco  15368  fucpropd  15383  initoval  15393  termoval  15394  homarcl  15424  coafval  15460  resssetc  15488  resscatc  15501  catciso  15503  xpcval  15563  1stfval  15577  2ndfval  15580  prfval  15585  prfcl  15589  evlfval  15603  curfval  15609  curf1cl  15614  curfcl  15618  uncf1  15622  uncf2  15623  diag12  15630  diag2  15631  curf2ndf  15633  hofval  15638  hof1  15640  hof2fval  15641  hofcl  15645  yon12  15651  yon2  15652  hofpropd  15653  joinval  15752  meetval  15766  isdlat  15940  plusffval  15994  grpidval  16004  grpidd  16012  gsumvalx  16014  gsumpropd  16016  gsumress  16020  ismndOLD  16043  ismndd  16060  issubmnd  16065  submnd0  16067  ismhm  16085  issubm  16095  resmhm  16107  resmhm2  16108  resmhm2b  16109  isgrp  16178  isgrpd2e  16189  grpidd2  16204  grpinvfval  16205  imasgrp2  16302  imasgrp  16303  subg0  16324  subginv  16325  subgcl  16328  issubgrpd2  16334  isnsg  16347  isghm  16384  resghm  16400  isga  16446  subgga  16455  gasubg  16457  cntzfval  16475  resscntz  16486  odfval  16674  gexval  16715  lsmfval  16775  lsmvalx  16776  oppglsm  16779  subglsm  16808  pj1fval  16829  efgtval  16858  iscmn  16922  iscmnd  16927  submcmn2  16964  iscyg  16999  issrg  17272  isring  17315  ringidss  17338  prdsmgp  17372  mulgass3  17399  dvdsrval  17407  isirred  17461  isdrngd  17534  isdrngrd  17535  subrg1  17552  subrgmcl  17554  subrgdvds  17556  subrguss  17557  subrginv  17558  subrgdv  17559  subrgunit  17560  subrgugrp  17561  abvfval  17580  isabvd  17582  issrngd  17623  islmod  17629  islmodd  17631  scaffval  17643  lmodpropd  17686  lssset  17693  islssd  17695  prdslmodd  17728  islmhm  17786  reslmhm  17811  reslmhm2  17812  reslmhm2b  17813  islbs  17835  rlmvneg  17966  rrgval  18048  isassa  18077  isassad  18085  assamulgscmlem2  18111  psrval  18124  resspsradd  18184  resspsrmul  18185  resspsrvsca  18186  mplmon2mul  18279  ply1coe  18450  ply1coeOLD  18451  lply1binomsc  18462  evl1expd  18494  evl1scvarpw  18512  isphl  18754  ipffval  18774  isphld  18780  ocvfval  18788  isobs  18842  frlmplusgval  18886  frlmsubgval  18887  frlmvscafval  18888  frlmip  18898  frlmipval  18899  frlmup1  18918  lsslindf  18950  mamufval  18972  matplusg2  19014  matvsca2  19015  matplusgcell  19020  matsubgcell  19021  matinvgcell  19022  matvscacell  19023  matmulcell  19032  mpt2matmul  19033  mat1  19034  mattposm  19046  mat1dimmul  19063  dmatmul  19084  dmatcrng  19089  scmataddcl  19103  scmatsubcl  19104  scmatcrng  19108  smatvscl  19111  scmatghm  19120  scmatmhm  19121  mvmulfval  19129  ma1repveval  19158  mdetrlin  19189  mdetrsca  19190  mdetmul  19210  madurid  19231  minmar1cl  19238  smadiadetglem1  19258  smadiadetr  19262  matinv  19264  slesolinv  19267  slesolinvbi  19268  cramerimplem3  19272  cpmatacl  19302  mat2pmatghm  19316  decpmatmullem  19357  decpmatmul  19358  pmatcollpw1lem1  19360  pmatcollpw2lem  19363  pmatcollpwlem  19366  pmatcollpw3lem  19369  mply1topmatval  19390  mp2pm2mplem1  19392  mp2pm2mplem4  19395  mp2pm2mplem5  19396  mp2pm2mp  19397  chpmat1d  19422  chpscmatgsummon  19431  chfacfpmmulgsum2  19451  xkocnv  20400  submtmd  20688  prdsdsf  20955  ressprdsds  20959  blfvalps  20971  prdsxmslem2  21117  tmsxpsval  21126  ngpds  21208  subgngp  21234  tngngp  21253  isnlm  21269  lssnlm  21294  isphtpy  21566  isphtpc  21579  pi1cpbl  21629  pi1addf  21632  pi1addval  21633  pi1grplem  21634  clmsub  21665  clmvsass  21672  clmvsdir  21673  cvsdiv  21694  iscph  21702  cphdir  21736  cphdi  21737  cph2di  21738  cph2subdi  21741  cphass  21742  tchval  21746  ipcau2  21762  tchcphlem1  21763  tchcphlem2  21764  caufval  21799  rrxip  21907  dvlip2  22481  q1pval  22639  r1pval  22642  dvntaylp  22851  efabl  23022  efsubm  23023  dchrmul  23640  istrkgc  23968  istrkgb  23969  istrkgcb  23970  istrkge  23971  istrkgl  23972  istrkg2d  23973  istrkgld  23974  iscgrg  24024  isismt  24041  tglngval  24058  legval  24091  mirval  24156  israg  24194  ishpg  24248  lmif  24271  islmib  24273  iscgra  24289  ttgval  24299  wlkon  24654  trlon  24663  trlonprop  24665  pthon  24698  pthonprop  24700  spthon  24705  spthonprp  24708  isconngra  24793  isconngra1  24794  is2wlkonot  24984  is2spthonot  24985  2wlkonot  24986  2spthonot  24987  2wlksot  24988  2spthsot  24989  2wlkonot3v  24996  2spthonot3v  24997  grpodivval  25362  gxval  25377  subgoov  25424  isrngo  25497  vcoprne  25589  dipfval  25729  ipval  25730  sspgval  25759  sspsval  25761  lnoval  25784  ajfval  25841  dipdir  25874  dipass  25877  htth  25952  isomnd  27844  submomnd  27853  inftmrel  27877  isinftm  27878  isslmd  27898  rngurd  27932  rdivmuldivd  27935  isorng  27943  suborng  27959  resv1r  27981  metidval  28023  pstmval  28028  pstmfval  28029  zlm0  28096  zlm1  28097  sitmval  28473  afsval  28734  mclsrcl  29110  mppsval  29121  istotbnd  30431  isbnd  30442  rrnequiv  30497  rngohomval  30533  idlval  30576  pridlval  30596  ismgmd  32782  ismgmhm  32789  issubmgm  32795  resmgmhm  32804  resmgmhm2  32805  resmgmhm2b  32806  idfusubc  32872  rnghmval  32897  lidlmsgrp  32932  lidlrng  32933  zlidlring  32934  uzlidlring  32935  rnghmresel  32972  rngchom  32975  rngcco  32979  rnghmsubcsetclem1  32983  rhmresel  33018  ringchom  33021  ringcco  33025  rhmsubcsetclem1  33029  rhmsubcrngclem1  33035  irinitoringc  33077  ovmpt2rdxf  33128  lincop  33209  lincval  33210  lincsum  33230  lincscm  33231  lmod1lem2  33289  lmod1lem3  33290  lmod1lem4  33291  ldepsnlinc  33309  lflset  35197  islfld  35200  ldualvadd  35267  ldualsmul  35273  ldualvs  35275  isopos  35318  cmtfvalN  35348  iscvlat  35461  ishlat1  35490  lineset  35875  psubspset  35881  paddfval  35934  paddval  35935  ltrnfset  36254  trnfsetN  36293  trlfset  36298  tgrpov  36887  erngplus  36942  erngmul  36945  erngplus-rN  36950  erngmul-rN  36953  erngdvlem3  37129  erngdvlem4  37130  erng0g  37133  erngdvlem3-rN  37137  erngdvlem4-rN  37138  dvaplusg  37148  dvamulr  37151  dvavadd  37154  dvavsca  37156  dvalveclem  37165  dvhmulr  37226  dvhfvadd  37231  dvhvadd  37232  dvhopvadd2  37234  dvhvaddcl  37235  dvhvaddcomN  37236  dvhvsca  37241  dvhlveclem  37248  dvh0g  37251  djavalN  37275  diblsmopel  37311  dicvaddcl  37330  cdlemn6  37342  dihffval  37370  dihopelvalcpre  37388  djhval  37538  lcdvaddval  37738  lcdsmul  37742  lcdvsval  37744  lcdlkreq2N  37763  hvmapffval  37898  hvmapfval  37899  hdmap1fval  37937  hgmapffval  38028  hgmapfval  38029  hgmapadd  38037  hlhilipval  38092  hlhilhillem  38103