Theorem oveqd 6325

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

Syntax hints:   -> wi 4   = wceq 1452  (class class class)co 6308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762  df-uni 4191  df-br 4396  df-iota 5553  df-fv 5597  df-ov 6311

This theorem is referenced by:  oveq123d  6329  oveqdr  6332  csbov  6343  csbov12g  6344  ovmpt2dxf  6441  oprssov  6457  ofeq  6552  fnmpt2ovd  6890  ruclem1  14360  vdwapval  15002  vdwapid1  15004  vdwmc2  15008  vdwpc  15009  vdwlem5  15014  vdwlem8  15017  vdwlem13  15022  prdsval  15431  prdsdsval2  15460  pwsplusgval  15466  pwsmulrval  15467  pwsvscafval  15470  imasval  15489  imasvalOLD  15490  iscat  15656  iscatd  15657  catidex  15658  catideu  15659  cidfval  15660  cidval  15661  catidd  15664  iscatd2  15665  catlid  15667  catrid  15668  homffval  15673  homfeqd  15678  homfeqval  15680  comfffval  15681  comffval  15682  comfeq  15689  comfeqd  15690  comfeqval  15691  catpropd  15692  oppcval  15696  oppcco  15700  monfval  15715  ismon  15716  oppcmon  15721  oppcepi  15722  sectffval  15733  sectfval  15734  invffval  15741  isoval  15748  dfiso2  15755  isofn  15758  invisoinvl  15773  invcoisoid  15775  isocoinvid  15776  issubc  15818  issubc3  15832  isfunc  15847  cofuval  15865  cofuval2  15870  funcres  15879  funcres2b  15880  funcres2  15881  funcres2c  15884  isfull  15893  isfth  15897  fullres2c  15922  natfval  15929  isnat  15930  fucval  15941  fucco  15945  fucpropd  15960  initoval  15970  termoval  15971  homarcl  16001  coafval  16037  resssetc  16065  resscatc  16078  catciso  16080  xpcval  16140  1stfval  16154  2ndfval  16157  prfval  16162  prfcl  16166  evlfval  16180  curfval  16186  curf1cl  16191  curfcl  16195  uncf1  16199  uncf2  16200  diag12  16207  diag2  16208  curf2ndf  16210  hofval  16215  hof1  16217  hof2fval  16218  hofcl  16222  yon12  16228  yon2  16229  hofpropd  16230  joinval  16329  meetval  16343  isdlat  16517  plusffval  16571  grpidval  16581  grpidd  16589  gsumvalx  16591  gsumpropd  16593  gsumress  16597  ismndOLD  16620  ismndd  16637  issubmnd  16642  submnd0  16644  ismhm  16662  issubm  16672  resmhm  16684  resmhm2  16685  resmhm2b  16686  isgrp  16755  isgrpd2e  16766  grpidd2  16781  grpinvfval  16782  imasgrp2  16879  imasgrp  16880  subg0  16901  subginv  16902  subgcl  16905  issubgrpd2  16911  isnsg  16924  isghm  16961  resghm  16977  isga  17023  subgga  17032  gasubg  17034  cntzfval  17052  resscntz  17063  odfval  17257  odfvalOLD  17260  gexval  17305  gexvalOLD  17307  lsmfval  17368  lsmvalx  17369  oppglsm  17372  subglsm  17401  pj1fval  17422  efgtval  17451  iscmn  17515  iscmnd  17520  submcmn2  17557  iscyg  17592  issrg  17819  isring  17862  ringidss  17885  prdsmgp  17916  mulgass3  17943  dvdsrval  17951  isirred  18005  isdrngd  18078  isdrngrd  18079  subrg1  18096  subrgmcl  18098  subrgdvds  18100  subrguss  18101  subrginv  18102  subrgdv  18103  subrgunit  18104  subrgugrp  18105  abvfval  18124  isabvd  18126  issrngd  18167  islmod  18173  islmodd  18175  scaffval  18187  lmodpropd  18229  lssset  18235  islssd  18237  prdslmodd  18270  islmhm  18328  reslmhm  18353  reslmhm2  18354  reslmhm2b  18355  islbs  18377  rlmvneg  18508  rrgval  18588  isassa  18616  isassad  18624  assamulgscmlem2  18650  psrval  18663  resspsradd  18717  resspsrmul  18718  resspsrvsca  18719  mplmon2mul  18801  ply1coe  18966  ply1coeOLD  18967  lply1binomsc  18978  evl1expd  19010  evl1scvarpw  19028  isphl  19272  ipffval  19292  isphld  19298  ocvfval  19306  isobs  19360  frlmplusgval  19403  frlmsubgval  19404  frlmvscafval  19405  frlmip  19413  frlmipval  19414  frlmup1  19433  lsslindf  19465  mamufval  19487  matplusg2  19529  matvsca2  19530  matplusgcell  19535  matsubgcell  19536  matinvgcell  19537  matvscacell  19538  matmulcell  19547  mpt2matmul  19548  mat1  19549  mattposm  19561  mat1dimmul  19578  dmatmul  19599  dmatcrng  19604  scmataddcl  19618  scmatsubcl  19619  scmatcrng  19623  smatvscl  19626  scmatghm  19635  scmatmhm  19636  mvmulfval  19644  ma1repveval  19673  mdetrlin  19704  mdetrsca  19705  mdetmul  19725  madurid  19746  minmar1cl  19753  smadiadetglem1  19773  smadiadetr  19777  matinv  19779  slesolinv  19782  slesolinvbi  19783  cramerimplem3  19787  cpmatacl  19817  mat2pmatghm  19831  decpmatmullem  19872  decpmatmul  19873  pmatcollpw1lem1  19875  pmatcollpw2lem  19878  pmatcollpwlem  19881  pmatcollpw3lem  19884  mply1topmatval  19905  mp2pm2mplem1  19907  mp2pm2mplem4  19910  mp2pm2mplem5  19911  mp2pm2mp  19912  chpmat1d  19937  chpscmatgsummon  19946  chfacfpmmulgsum2  19966  xkocnv  20906  submtmd  21197  prdsdsf  21460  ressprdsds  21464  blfvalps  21476  prdsxmslem2  21622  tmsxpsval  21631  ngpds  21695  subgngp  21721  tngngp  21740  isnlm  21756  lssnlm  21781  isphtpy  22090  isphtpc  22103  pi1cpbl  22153  pi1addf  22156  pi1addval  22157  pi1grplem  22158  clmsub  22189  clmvsass  22196  clmvsdir  22197  cvsdiv  22218  iscph  22226  cphdir  22260  cphdi  22261  cph2di  22262  cph2subdi  22265  cphass  22266  tchval  22270  ipcau2  22286  tchcphlem1  22287  tchcphlem2  22288  caufval  22323  rrxip  22427  dvlip2  23026  q1pval  23183  r1pval  23186  dvntaylp  23405  efabl  23578  efsubm  23579  dchrmul  24255  istrkgc  24581  istrkgb  24582  istrkgcb  24583  istrkge  24584  istrkgl  24585  istrkgld  24586  iscgrg  24636  isismt  24658  tglngval  24675  legval  24708  ishlg  24726  mirval  24779  israg  24821  ishpg  24880  lmif  24906  islmib  24908  isinag  24958  ttgval  24984  wlkon  25340  trlon  25349  trlonprop  25351  pthon  25384  pthonprop  25386  spthon  25391  spthonprp  25394  isconngra  25479  isconngra1  25480  is2wlkonot  25670  is2spthonot  25671  2wlkonot  25672  2spthonot  25673  2wlksot  25674  2spthsot  25675  2wlkonot3v  25682  2spthonot3v  25683  grpodivval  26052  gxval  26067  subgoov  26114  isrngo  26187  vcoprne  26279  dipfval  26419  ipval  26420  sspgval  26449  sspsval  26451  lnoval  26474  ajfval  26531  dipdir  26564  dipass  26567  htth  26652  isomnd  28538  submomnd  28547  inftmrel  28571  isinftm  28572  isslmd  28592  rngurd  28625  rdivmuldivd  28628  isorng  28636  suborng  28652  resv1r  28674  smatlem  28697  submatminr1  28710  metidval  28767  pstmval  28772  pstmfval  28773  zlm0  28840  zlm1  28841  sitmval  29255  istrkg2d  29555  afsval  29560  mclsrcl  30271  mppsval  30282  istotbnd  32165  isbnd  32176  rrnequiv  32231  rngohomval  32267  idlval  32310  pridlval  32330  lflset  32696  islfld  32699  ldualvadd  32766  ldualsmul  32772  ldualvs  32774  isopos  32817  cmtfvalN  32847  iscvlat  32960  ishlat1  32989  lineset  33374  psubspset  33380  paddfval  33433  paddval  33434  ltrnfset  33753  trnfsetN  33792  trlfset  33797  tgrpov  34386  erngplus  34441  erngmul  34444  erngplus-rN  34449  erngmul-rN  34452  erngdvlem3  34628  erngdvlem4  34629  erng0g  34632  erngdvlem3-rN  34636  erngdvlem4-rN  34637  dvaplusg  34647  dvamulr  34650  dvavadd  34653  dvavsca  34655  dvalveclem  34664  dvhmulr  34725  dvhfvadd  34730  dvhvadd  34731  dvhopvadd2  34733  dvhvaddcl  34734  dvhvaddcomN  34735  dvhvsca  34740  dvhlveclem  34747  dvh0g  34750  djavalN  34774  diblsmopel  34810  dicvaddcl  34829  cdlemn6  34841  dihffval  34869  dihopelvalcpre  34887  djhval  35037  lcdvaddval  35237  lcdsmul  35241  lcdvsval  35243  lcdlkreq2N  35262  hvmapffval  35397  hvmapfval  35398  hdmap1fval  35436  hgmapffval  35527  hgmapfval  35528  hgmapadd  35536  hlhilipval  35591  hlhilhillem  35602  hoidmvval0b  38530  hoidmvlelem2  38536  hoidmvlelem3  38537  hoidmvle  38540  ovnhoi  38543  hoiqssbl  38565  hspmbllem2  38567  mptmpt2opabbrd  39180  mptmpt2opabovd  39181  1wlksonproplem  39900  isconngr  40103  isconngr1  40104  ismgmd  40284  ismgmhm  40291  issubmgm  40297  resmgmhm  40306  resmgmhm2  40307  resmgmhm2b  40308  idfusubc  40374  rnghmval  40399  lidlmsgrp  40434  lidlrng  40435  zlidlring  40436  uzlidlring  40437  rnghmresel  40474  rngchom  40477  rngcco  40481  rnghmsubcsetclem1  40485  rhmresel  40520  ringchom  40523  ringcco  40527  rhmsubcsetclem1  40531  rhmsubcrngclem1  40537  irinitoringc  40579  ovmpt2rdxf  40628  lincop  40709  lincval  40710  lincsum  40730  lincscm  40731  lmod1lem2  40789  lmod1lem3  40790  lmod1lem4  40791  ldepsnlinc  40809