Theorem oveqd 6103

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 6092	. 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 1369  (class class class)co 6086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089

This theorem is referenced by:  oveq123d  6107  csbov  6118  csbov12g  6120  ovmpt2dxf  6211  oprssov  6227  ofeq  6317  fnmpt2ovd  6646  ruclem1  13505  vdwapval  14026  vdwapid1  14028  vdwmc2  14032  vdwpc  14033  vdwlem5  14038  vdwlem8  14041  vdwlem13  14046  prdsval  14385  prdsdsval2  14414  pwsplusgval  14420  pwsmulrval  14421  pwsvscafval  14424  imasval  14441  iscat  14602  iscatd  14603  catidex  14604  catideu  14605  cidfval  14606  cidval  14607  catidd  14610  iscatd2  14611  catlid  14613  catrid  14614  proplem3  14621  homffval  14622  homfeqd  14626  homfeqval  14628  comfffval  14629  comffval  14630  comfeq  14637  comfeqd  14638  comfeqval  14639  catpropd  14640  oppcval  14644  oppcco  14648  monfval  14663  ismon  14664  oppcmon  14669  oppcepi  14670  sectffval  14681  sectfval  14682  invffval  14688  isoval  14695  issubc  14740  issubc3  14751  isfunc  14766  cofuval  14784  cofuval2  14789  funcres  14798  funcres2b  14799  funcres2  14800  funcres2c  14803  isfull  14812  isfth  14816  fullres2c  14841  natfval  14848  isnat  14849  fucval  14860  fucco  14864  fucpropd  14879  homarcl  14888  coafval  14924  resssetc  14952  resscatc  14965  catciso  14967  xpcval  14979  1stfval  14993  2ndfval  14996  prfval  15001  prfcl  15005  evlfval  15019  curfval  15025  curf1cl  15030  curfcl  15034  uncf1  15038  uncf2  15039  diag12  15046  diag2  15047  curf2ndf  15049  hofval  15054  hof1  15056  hof2fval  15057  hofcl  15061  yon12  15067  yon2  15068  hofpropd  15069  joinval  15167  meetval  15181  isdlat  15355  ismnd  15409  plusffval  15419  grpidval  15424  grpidd  15435  ismndd  15436  issubmnd  15441  submnd0  15443  ismhm  15458  issubm  15466  resmhm  15478  resmhm2  15479  resmhm2b  15480  gsumvalx  15493  gsumpropd  15495  gsumress  15498  isgrp  15540  isgrpd2e  15551  grpidd2  15566  grpinvfval  15567  imasgrp2  15661  imasgrp  15662  subg0  15678  subginv  15679  subgcl  15682  issubgrpd2  15688  isnsg  15701  isghm  15738  resghm  15754  isga  15800  subgga  15809  gasubg  15811  cntzfval  15829  resscntz  15840  odfval  16027  gexval  16068  lsmfval  16128  lsmvalx  16129  oppglsm  16132  subglsm  16161  pj1fval  16182  efgtval  16211  iscmn  16275  iscmnd  16280  submcmn2  16314  iscyg  16347  issrg  16597  isrng  16637  rngidss  16659  prdsmgp  16690  mulgass3  16717  dvdsrval  16725  isirred  16779  isdrngd  16835  isdrngrd  16836  subrg1  16853  subrgmcl  16855  subrgdvds  16857  subrguss  16858  subrginv  16859  subrgdv  16860  subrgunit  16861  subrgugrp  16862  abvfval  16881  isabvd  16883  issrngd  16924  islmod  16930  islmodd  16932  scaffval  16944  lmodpropd  16986  lssset  16992  islssd  16994  prdslmodd  17027  islmhm  17085  reslmhm  17110  reslmhm2  17111  reslmhm2b  17112  islbs  17134  rlmvneg  17265  rrgval  17335  isassa  17364  isassad  17371  psrval  17406  resspsradd  17465  resspsrmul  17466  resspsrvsca  17467  mplmon2mul  17558  ply1coe  17721  ply1coeOLD  17722  evl1expd  17754  evl1scvarpw  17772  isphl  18032  ipffval  18052  isphld  18058  ocvfval  18066  isobs  18120  frlmplusgval  18166  frlmsubgval  18167  frlmvscafval  18168  frlmip  18178  frlmipval  18179  frlmup1  18201  lsslindf  18234  mamufval  18258  matplusg2  18302  matvsca2  18303  mat1  18309  mattposm  18319  mvmulfval  18328  ma1repveval  18357  mdetrlin  18384  mdetrsca  18385  mdetmul  18404  madurid  18425  minmar1cl  18432  smadiadetglem1  18452  smadiadetr  18456  matinv  18458  slesolinv  18461  slesolinvbi  18462  cramerimplem3  18466  xkocnv  19362  submtmd  19650  prdsdsf  19917  ressprdsds  19921  blfvalps  19933  prdsxmslem2  20079  tmsxpsval  20088  ngpds  20170  subgngp  20196  tngngp  20215  isnlm  20231  lssnlm  20256  isphtpy  20528  isphtpc  20541  pi1cpbl  20591  pi1addf  20594  pi1addval  20595  pi1grplem  20596  clmsub  20627  clmvsass  20634  clmvsdir  20635  cvsdiv  20656  iscph  20664  cphdir  20698  cphdi  20699  cph2di  20700  cph2subdi  20703  cphass  20704  tchval  20708  ipcau2  20724  tchcphlem1  20725  tchcphlem2  20726  caufval  20761  rrxip  20869  dvlip2  21442  q1pval  21600  r1pval  21603  dvntaylp  21811  dchrmul  22562  istrkgc  22892  istrkgb  22893  istrkgcb  22894  istrkge  22895  istrkgl  22896  istrkg2d  22897  iscgrg  22940  tglngval  22959  legval  22986  mirval  23027  israg  23056  ttgval  23072  wlkon  23380  trlon  23390  trlonprop  23392  pthon  23425  pthonprop  23427  spthon  23432  spthonprp  23435  isconngra  23509  isconngra1  23510  grpodivval  23681  gxval  23696  subgoov  23743  isrngo  23816  vcoprne  23908  dipfval  24048  ipval  24049  sspgval  24078  sspsval  24080  lnoval  24103  ajfval  24160  dipdir  24193  dipass  24196  htth  24271  isomnd  26115  submomnd  26124  inftmrel  26148  isinftm  26149  isslmd  26169  rngurd  26207  rdivmuldivd  26210  isorng  26218  suborng  26234  resv0g  26256  resv1r  26257  resvcmn  26258  metidval  26269  pstmval  26274  pstmfval  26275  zlm0  26343  zlm1  26344  sitmval  26686  afsval  26947  istotbnd  28621  isbnd  28632  rrnequiv  28687  rngohomval  28723  idlval  28766  pridlval  28786  is2wlkonot  30335  is2spthonot  30336  2wlkonot  30337  2spthonot  30338  2wlksot  30339  2spthsot  30340  2wlkonot3v  30347  2spthonot3v  30348  ovmpt2rdxf  30681  assamulgscmlem2  30760  lply1binomsc  30775  matplusgcell  30782  matsubgcell  30783  matvscacell  30784  mat1dimmul  30795  dmatmul  30799  dmatcrng  30804  scmatcrng  30811  pmatcollpw2lem  30820  lincop  30831  lincval  30832  lincsum  30852  lincscm  30853  lmod1lem1  30918  lmod1lem2  30919  lmod1lem3  30920  lmod1lem4  30921  lmod1lem5  30922  ldepsnlinc  30939  lflset  32544  islfld  32547  ldualvadd  32614  ldualsmul  32620  ldualvs  32622  isopos  32665  cmtfvalN  32695  iscvlat  32808  ishlat1  32837  lineset  33222  psubspset  33228  paddfval  33281  paddval  33282  ltrnfset  33601  trnfsetN  33639  trlfset  33644  tgrpov  34232  erngplus  34287  erngmul  34290  erngplus-rN  34295  erngmul-rN  34298  erngdvlem3  34474  erngdvlem4  34475  erng0g  34478  erngdvlem3-rN  34482  erngdvlem4-rN  34483  dvaplusg  34493  dvamulr  34496  dvavadd  34499  dvavsca  34501  dvalveclem  34510  dvhmulr  34571  dvhfvadd  34576  dvhvadd  34577  dvhopvadd2  34579  dvhvaddcl  34580  dvhvaddcomN  34581  dvhvsca  34586  dvhlveclem  34593  dvh0g  34596  djavalN  34620  diblsmopel  34656  dicvaddcl  34675  cdlemn6  34687  dihffval  34715  dihopelvalcpre  34733  djhval  34883  lcdvaddval  35083  lcdsmul  35087  lcdvsval  35089  lcdlkreq2N  35108  hvmapffval  35243  hvmapfval  35244  hdmap1fval  35282  hgmapffval  35373  hgmapfval  35374  hgmapadd  35382  hlhilipval  35437  hlhilhillem  35448