Theorem oveqd 6057

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 6046	. 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 1649  (class class class)co 6040

This theorem is referenced by:  oveq123d  6061  csbov12g  6072  ovmpt2dxf  6158  oprssov  6174  ofeq  6266  ruclem1  12785  vdwapval  13296  vdwapid1  13298  vdwmc2  13302  vdwpc  13303  vdwlem5  13308  vdwlem8  13311  vdwlem13  13316  prdsval  13633  prdsdsval2  13661  pwsplusgval  13667  pwsmulrval  13668  pwsvscafval  13671  imasval  13692  iscat  13852  iscatd  13853  catidex  13854  catideu  13855  cidfval  13856  cidval  13857  catidd  13860  iscatd2  13861  catlid  13863  catrid  13864  proplem3  13871  homffval  13872  homfeqd  13876  homfeqval  13878  comfffval  13879  comffval  13880  comfeq  13887  comfeqd  13888  comfeqval  13889  catpropd  13890  oppcval  13894  oppcco  13898  monfval  13913  ismon  13914  oppcmon  13919  oppcepi  13920  sectffval  13931  sectfval  13932  invffval  13938  isoval  13945  issubc  13990  issubc3  14001  isfunc  14016  cofuval  14034  cofuval2  14039  funcres  14048  funcres2b  14049  funcres2  14050  funcres2c  14053  isfull  14062  isfth  14066  fullres2c  14091  natfval  14098  isnat  14099  fucval  14110  fucco  14114  fucpropd  14129  homarcl  14138  coafval  14174  resssetc  14202  resscatc  14215  catciso  14217  xpcval  14229  1stfval  14243  2ndfval  14246  prfval  14251  prfcl  14255  evlfval  14269  curfval  14275  curf1cl  14280  curfcl  14284  uncf1  14288  uncf2  14289  diag12  14296  diag2  14297  curf2ndf  14299  hofval  14304  hof1  14306  hof2fval  14307  hofcl  14311  yon12  14317  yon2  14318  hofpropd  14319  joinval  14400  meetval  14407  islat  14431  isdlat  14574  ismnd  14647  plusffval  14657  grpidval  14662  grpidd  14673  ismndd  14674  issubmnd  14679  submnd0  14680  ismhm  14695  issubm  14703  resmhm  14714  resmhm2  14715  resmhm2b  14716  gsumvalx  14729  gsumpropd  14731  gsumress  14732  isgrp  14771  isgrpd2e  14782  grpidd2  14797  grpinvfval  14798  imasgrp2  14888  imasgrp  14889  subg0  14905  subginv  14906  subgcl  14909  isnsg  14924  isghm  14961  resghm  14977  isga  15023  subgga  15032  gasubg  15034  cntzfval  15074  resscntz  15085  odfval  15126  gexval  15167  lsmfval  15227  lsmvalx  15228  oppglsm  15231  subglsm  15260  pj1fval  15281  efgtval  15310  iscmn  15374  iscmnd  15379  submcmn2  15413  iscyg  15444  isrng  15623  rngidss  15645  prdsmgp  15671  mulgass3  15697  dvdsrval  15705  isirred  15759  isdrngd  15815  isdrngrd  15816  subrg1  15833  subrgmcl  15835  subrgdvds  15837  subrguss  15838  subrginv  15839  subrgdv  15840  subrgunit  15841  subrgugrp  15842  abvfval  15861  isabvd  15863  issrngd  15904  islmod  15909  islmodd  15911  scaffval  15923  lmodpropd  15962  lssset  15965  islssd  15967  prdslmodd  16000  islmhm  16058  reslmhm  16083  reslmhm2  16084  reslmhm2b  16085  islbs  16103  issubgrpd2  16215  rlmvneg  16233  rrgval  16302  isassa  16330  isassad  16337  psrval  16384  resspsradd  16434  resspsrmul  16435  resspsrvsca  16436  mplmon2mul  16516  ply1coe  16639  isphl  16814  ipffval  16834  isphld  16840  ocvfval  16848  isobs  16902  xkocnv  17799  submtmd  18087  prdsdsf  18350  ressprdsds  18354  blfvalps  18366  prdsxmslem2  18512  tmsxpsval  18521  ngpds  18603  subgngp  18629  tngngp  18648  isnlm  18664  lssnlm  18689  isphtpy  18959  isphtpc  18972  pi1cpbl  19022  pi1addf  19025  pi1addval  19026  pi1grplem  19027  clmsub  19058  clmvsass  19065  clmvsdir  19066  iscph  19086  cphdir  19120  cphdi  19121  cph2di  19122  cph2subdi  19125  cphass  19126  tchval  19130  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  caufval  19181  dvlip2  19832  evl1expd  19911  q1pval  20029  r1pval  20032  dvntaylp  20240  dchrmul  20985  wlkon  21483  trlon  21493  trlonprop  21495  pthon  21528  pthonprop  21530  spthon  21535  spthonprp  21538  isconngra  21612  isconngra1  21613  grpodivval  21784  gxval  21799  subgoov  21846  isrngo  21919  vcoprne  22011  dipfval  22151  ipval  22152  sspgval  22181  sspsval  22183  lnoval  22206  ajfval  22263  dipdir  22296  dipass  22299  htth  22374  rdivmuldivd  24180  isofld  24188  subofld  24198  inftmrel  24203  isinftm  24204  metidval  24238  pstmval  24243  pstmfval  24244  zlm0  24299  zlm1  24300  sitmval  24614  istotbnd  26368  isbnd  26379  rrnequiv  26434  rngohomval  26470  idlval  26513  pridlval  26533  frlmplusgval  27097  frlmvscafval  27098  frlmup1  27118  lsslindf  27168  mamufval  27311  matplusg2  27345  matvsca2  27346  mat1  27350  is2wlkonot  28060  is2spthonot  28061  2wlkonot  28062  2spthonot  28063  2wlksot  28064  2spthsot  28065  2wlkonot3v  28072  2spthonot3v  28073  lflset  29542  islfld  29545  ldualvadd  29612  ldualsmul  29618  ldualvs  29620  isopos  29663  cmtfvalN  29693  iscvlat  29806  ishlat1  29835  lineset  30220  psubspset  30226  paddfval  30279  paddval  30280  ltrnfset  30599  trnfsetN  30637  trlfset  30642  tgrpov  31230  erngplus  31285  erngmul  31288  erngplus-rN  31293  erngmul-rN  31296  erngdvlem3  31472  erngdvlem4  31473  erng0g  31476  erngdvlem3-rN  31480  erngdvlem4-rN  31481  dvaplusg  31491  dvamulr  31494  dvavadd  31497  dvavsca  31499  dvalveclem  31508  dvhmulr  31569  dvhfvadd  31574  dvhvadd  31575  dvhopvadd2  31577  dvhvaddcl  31578  dvhvaddcomN  31579  dvhvsca  31584  dvhlveclem  31591  dvh0g  31594  djavalN  31618  diblsmopel  31654  dicvaddcl  31673  cdlemn6  31685  dihffval  31713  dihopelvalcpre  31731  djhval  31881  lcdvaddval  32081  lcdsmul  32085  lcdvsval  32087  lcdlkreq2N  32106  hvmapffval  32241  hvmapfval  32242  hdmap1fval  32280  hgmapffval  32371  hgmapfval  32372  hgmapadd  32380  hlhilipval  32435  hlhilhillem  32446

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043