Theorem oveqd 6301

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 6290	. 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 1379  (class class class)co 6284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287

This theorem is referenced by:  oveq123d  6305  csbov  6316  csbov12g  6318  ovmpt2dxf  6412  oprssov  6428  ofeq  6526  fnmpt2ovd  6861  ruclem1  13825  vdwapval  14350  vdwapid1  14352  vdwmc2  14356  vdwpc  14357  vdwlem5  14362  vdwlem8  14365  vdwlem13  14370  prdsval  14710  prdsdsval2  14739  pwsplusgval  14745  pwsmulrval  14746  pwsvscafval  14749  imasval  14766  iscat  14927  iscatd  14928  catidex  14929  catideu  14930  cidfval  14931  cidval  14932  catidd  14935  iscatd2  14936  catlid  14938  catrid  14939  proplem3  14946  homffval  14947  homfeqd  14951  homfeqval  14953  comfffval  14954  comffval  14955  comfeq  14962  comfeqd  14963  comfeqval  14964  catpropd  14965  oppcval  14969  oppcco  14973  monfval  14988  ismon  14989  oppcmon  14994  oppcepi  14995  sectffval  15006  sectfval  15007  invffval  15013  isoval  15020  issubc  15065  issubc3  15076  isfunc  15091  cofuval  15109  cofuval2  15114  funcres  15123  funcres2b  15124  funcres2  15125  funcres2c  15128  isfull  15137  isfth  15141  fullres2c  15166  natfval  15173  isnat  15174  fucval  15185  fucco  15189  fucpropd  15204  homarcl  15213  coafval  15249  resssetc  15277  resscatc  15290  catciso  15292  xpcval  15304  1stfval  15318  2ndfval  15321  prfval  15326  prfcl  15330  evlfval  15344  curfval  15350  curf1cl  15355  curfcl  15359  uncf1  15363  uncf2  15364  diag12  15371  diag2  15372  curf2ndf  15374  hofval  15379  hof1  15381  hof2fval  15382  hofcl  15386  yon12  15392  yon2  15393  hofpropd  15394  joinval  15492  meetval  15506  isdlat  15680  ismnd  15734  plusffval  15744  grpidval  15749  grpidd  15760  ismndd  15761  issubmnd  15767  submnd0  15769  ismhm  15788  issubm  15797  resmhm  15809  resmhm2  15810  resmhm2b  15811  gsumvalx  15824  gsumpropd  15826  gsumress  15829  isgrp  15871  isgrpd2e  15882  grpidd2  15897  grpinvfval  15898  imasgrp2  15995  imasgrp  15996  subg0  16012  subginv  16013  subgcl  16016  issubgrpd2  16022  isnsg  16035  isghm  16072  resghm  16088  isga  16134  subgga  16143  gasubg  16145  cntzfval  16163  resscntz  16174  odfval  16363  gexval  16404  lsmfval  16464  lsmvalx  16465  oppglsm  16468  subglsm  16497  pj1fval  16518  efgtval  16547  iscmn  16611  iscmnd  16616  submcmn2  16650  iscyg  16685  issrg  16961  isrng  17004  rngidss  17026  prdsmgp  17060  mulgass3  17087  dvdsrval  17095  isirred  17149  isdrngd  17221  isdrngrd  17222  subrg1  17239  subrgmcl  17241  subrgdvds  17243  subrguss  17244  subrginv  17245  subrgdv  17246  subrgunit  17247  subrgugrp  17248  abvfval  17267  isabvd  17269  issrngd  17310  islmod  17316  islmodd  17318  scaffval  17330  lmodpropd  17373  lssset  17380  islssd  17382  prdslmodd  17415  islmhm  17473  reslmhm  17498  reslmhm2  17499  reslmhm2b  17500  islbs  17522  rlmvneg  17653  rrgval  17734  isassa  17763  isassad  17771  assamulgscmlem2  17797  psrval  17810  resspsradd  17870  resspsrmul  17871  resspsrvsca  17872  mplmon2mul  17965  ply1coe  18136  ply1coeOLD  18137  lply1binomsc  18148  evl1expd  18180  evl1scvarpw  18198  isphl  18458  ipffval  18478  isphld  18484  ocvfval  18492  isobs  18546  frlmplusgval  18592  frlmsubgval  18593  frlmvscafval  18594  frlmip  18604  frlmipval  18605  frlmup1  18627  lsslindf  18660  mamufval  18682  matplusg2  18724  matvsca2  18725  matplusgcell  18730  matsubgcell  18731  matinvgcell  18732  matvscacell  18733  matmulcell  18742  mpt2matmul  18743  mat1  18744  mattposm  18756  mat1dimmul  18773  dmatmul  18794  dmatcrng  18799  scmatscm  18810  scmataddcl  18813  scmatsubcl  18814  scmatcrng  18818  smatvscl  18821  scmatghm  18830  scmatmhm  18831  mvmulfval  18839  ma1repveval  18868  mdetrlin  18899  mdetrsca  18900  mdetmul  18920  madurid  18941  minmar1cl  18948  smadiadetglem1  18968  smadiadetr  18972  matinv  18974  slesolinv  18977  slesolinvbi  18978  cramerimplem3  18982  cpmatacl  19012  mat2pmatghm  19026  decpmatmullem  19067  decpmatmul  19068  pmatcollpw1lem1  19070  pmatcollpw2lem  19073  pmatcollpwlem  19076  pmatcollpw3lem  19079  mply1topmatval  19100  mp2pm2mplem1  19102  mp2pm2mplem4  19105  mp2pm2mplem5  19106  mp2pm2mp  19107  chpmat1d  19132  chpscmatgsummon  19141  chfacfpmmulgsum2  19161  xkocnv  20078  submtmd  20366  prdsdsf  20633  ressprdsds  20637  blfvalps  20649  prdsxmslem2  20795  tmsxpsval  20804  ngpds  20886  subgngp  20912  tngngp  20931  isnlm  20947  lssnlm  20972  isphtpy  21244  isphtpc  21257  pi1cpbl  21307  pi1addf  21310  pi1addval  21311  pi1grplem  21312  clmsub  21343  clmvsass  21350  clmvsdir  21351  cvsdiv  21372  iscph  21380  cphdir  21414  cphdi  21415  cph2di  21416  cph2subdi  21419  cphass  21420  tchval  21424  ipcau2  21440  tchcphlem1  21441  tchcphlem2  21442  caufval  21477  rrxip  21585  dvlip2  22159  q1pval  22317  r1pval  22320  dvntaylp  22528  dchrmul  23279  istrkgc  23607  istrkgb  23608  istrkgcb  23609  istrkge  23610  istrkgl  23611  istrkg2d  23612  istrkgld  23613  iscgrg  23660  isismt  23677  tglngval  23694  legval  23726  mirval  23777  israg  23810  lmif  23856  islmib  23858  ttgval  23882  wlkon  24237  trlon  24246  trlonprop  24248  pthon  24281  pthonprop  24283  spthon  24288  spthonprp  24291  isconngra  24376  isconngra1  24377  is2wlkonot  24567  is2spthonot  24568  2wlkonot  24569  2spthonot  24570  2wlksot  24571  2spthsot  24572  2wlkonot3v  24579  2spthonot3v  24580  grpodivval  24949  gxval  24964  subgoov  25011  isrngo  25084  vcoprne  25176  dipfval  25316  ipval  25317  sspgval  25346  sspsval  25348  lnoval  25371  ajfval  25428  dipdir  25461  dipass  25464  htth  25539  isomnd  27381  submomnd  27390  inftmrel  27414  isinftm  27415  isslmd  27435  rngurd  27469  rdivmuldivd  27472  isorng  27480  suborng  27496  resv0g  27517  resv1r  27518  resvcmn  27519  metidval  27533  pstmval  27538  pstmfval  27539  zlm0  27607  zlm1  27608  sitmval  27958  afsval  28219  istotbnd  29896  isbnd  29907  rrnequiv  29962  rngohomval  29998  idlval  30041  pridlval  30061  ovmpt2rdxf  32024  lincop  32108  lincval  32109  lincsum  32129  lincscm  32130  lmod1lem1  32187  lmod1lem2  32188  lmod1lem3  32189  lmod1lem4  32190  lmod1lem5  32191  ldepsnlinc  32208  lflset  33874  islfld  33877  ldualvadd  33944  ldualsmul  33950  ldualvs  33952  isopos  33995  cmtfvalN  34025  iscvlat  34138  ishlat1  34167  lineset  34552  psubspset  34558  paddfval  34611  paddval  34612  ltrnfset  34931  trnfsetN  34969  trlfset  34974  tgrpov  35562  erngplus  35617  erngmul  35620  erngplus-rN  35625  erngmul-rN  35628  erngdvlem3  35804  erngdvlem4  35805  erng0g  35808  erngdvlem3-rN  35812  erngdvlem4-rN  35813  dvaplusg  35823  dvamulr  35826  dvavadd  35829  dvavsca  35831  dvalveclem  35840  dvhmulr  35901  dvhfvadd  35906  dvhvadd  35907  dvhopvadd2  35909  dvhvaddcl  35910  dvhvaddcomN  35911  dvhvsca  35916  dvhlveclem  35923  dvh0g  35926  djavalN  35950  diblsmopel  35986  dicvaddcl  36005  cdlemn6  36017  dihffval  36045  dihopelvalcpre  36063  djhval  36213  lcdvaddval  36413  lcdsmul  36417  lcdvsval  36419  lcdlkreq2N  36438  hvmapffval  36573  hvmapfval  36574  hdmap1fval  36612  hgmapffval  36703  hgmapfval  36704  hgmapadd  36712  hlhilipval  36767  hlhilhillem  36778