Theorem oveqd 6307

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 6296	. 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 1444  (class class class)co 6290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293

This theorem is referenced by:  oveq123d  6311  oveqdr  6314  csbov  6325  csbov12g  6326  ovmpt2dxf  6422  oprssov  6438  ofeq  6533  fnmpt2ovd  6871  ruclem1  14283  vdwapval  14923  vdwapid1  14925  vdwmc2  14929  vdwpc  14930  vdwlem5  14935  vdwlem8  14938  vdwlem13  14943  prdsval  15353  prdsdsval2  15382  pwsplusgval  15388  pwsmulrval  15389  pwsvscafval  15392  imasval  15411  imasvalOLD  15412  iscat  15578  iscatd  15579  catidex  15580  catideu  15581  cidfval  15582  cidval  15583  catidd  15586  iscatd2  15587  catlid  15589  catrid  15590  homffval  15595  homfeqd  15600  homfeqval  15602  comfffval  15603  comffval  15604  comfeq  15611  comfeqd  15612  comfeqval  15613  catpropd  15614  oppcval  15618  oppcco  15622  monfval  15637  ismon  15638  oppcmon  15643  oppcepi  15644  sectffval  15655  sectfval  15656  invffval  15663  isoval  15670  dfiso2  15677  isofn  15680  invisoinvl  15695  invcoisoid  15697  isocoinvid  15698  issubc  15740  issubc3  15754  isfunc  15769  cofuval  15787  cofuval2  15792  funcres  15801  funcres2b  15802  funcres2  15803  funcres2c  15806  isfull  15815  isfth  15819  fullres2c  15844  natfval  15851  isnat  15852  fucval  15863  fucco  15867  fucpropd  15882  initoval  15892  termoval  15893  homarcl  15923  coafval  15959  resssetc  15987  resscatc  16000  catciso  16002  xpcval  16062  1stfval  16076  2ndfval  16079  prfval  16084  prfcl  16088  evlfval  16102  curfval  16108  curf1cl  16113  curfcl  16117  uncf1  16121  uncf2  16122  diag12  16129  diag2  16130  curf2ndf  16132  hofval  16137  hof1  16139  hof2fval  16140  hofcl  16144  yon12  16150  yon2  16151  hofpropd  16152  joinval  16251  meetval  16265  isdlat  16439  plusffval  16493  grpidval  16503  grpidd  16511  gsumvalx  16513  gsumpropd  16515  gsumress  16519  ismndOLD  16542  ismndd  16559  issubmnd  16564  submnd0  16566  ismhm  16584  issubm  16594  resmhm  16606  resmhm2  16607  resmhm2b  16608  isgrp  16677  isgrpd2e  16688  grpidd2  16703  grpinvfval  16704  imasgrp2  16801  imasgrp  16802  subg0  16823  subginv  16824  subgcl  16827  issubgrpd2  16833  isnsg  16846  isghm  16883  resghm  16899  isga  16945  subgga  16954  gasubg  16956  cntzfval  16974  resscntz  16985  odfval  17179  odfvalOLD  17182  gexval  17227  gexvalOLD  17229  lsmfval  17290  lsmvalx  17291  oppglsm  17294  subglsm  17323  pj1fval  17344  efgtval  17373  iscmn  17437  iscmnd  17442  submcmn2  17479  iscyg  17514  issrg  17741  isring  17784  ringidss  17807  prdsmgp  17838  mulgass3  17865  dvdsrval  17873  isirred  17927  isdrngd  18000  isdrngrd  18001  subrg1  18018  subrgmcl  18020  subrgdvds  18022  subrguss  18023  subrginv  18024  subrgdv  18025  subrgunit  18026  subrgugrp  18027  abvfval  18046  isabvd  18048  issrngd  18089  islmod  18095  islmodd  18097  scaffval  18109  lmodpropd  18151  lssset  18157  islssd  18159  prdslmodd  18192  islmhm  18250  reslmhm  18275  reslmhm2  18276  reslmhm2b  18277  islbs  18299  rlmvneg  18430  rrgval  18511  isassa  18539  isassad  18547  assamulgscmlem2  18573  psrval  18586  resspsradd  18640  resspsrmul  18641  resspsrvsca  18642  mplmon2mul  18724  ply1coe  18889  ply1coeOLD  18890  lply1binomsc  18901  evl1expd  18933  evl1scvarpw  18951  isphl  19195  ipffval  19215  isphld  19221  ocvfval  19229  isobs  19283  frlmplusgval  19326  frlmsubgval  19327  frlmvscafval  19328  frlmip  19336  frlmipval  19337  frlmup1  19356  lsslindf  19388  mamufval  19410  matplusg2  19452  matvsca2  19453  matplusgcell  19458  matsubgcell  19459  matinvgcell  19460  matvscacell  19461  matmulcell  19470  mpt2matmul  19471  mat1  19472  mattposm  19484  mat1dimmul  19501  dmatmul  19522  dmatcrng  19527  scmataddcl  19541  scmatsubcl  19542  scmatcrng  19546  smatvscl  19549  scmatghm  19558  scmatmhm  19559  mvmulfval  19567  ma1repveval  19596  mdetrlin  19627  mdetrsca  19628  mdetmul  19648  madurid  19669  minmar1cl  19676  smadiadetglem1  19696  smadiadetr  19700  matinv  19702  slesolinv  19705  slesolinvbi  19706  cramerimplem3  19710  cpmatacl  19740  mat2pmatghm  19754  decpmatmullem  19795  decpmatmul  19796  pmatcollpw1lem1  19798  pmatcollpw2lem  19801  pmatcollpwlem  19804  pmatcollpw3lem  19807  mply1topmatval  19828  mp2pm2mplem1  19830  mp2pm2mplem4  19833  mp2pm2mplem5  19834  mp2pm2mp  19835  chpmat1d  19860  chpscmatgsummon  19869  chfacfpmmulgsum2  19889  xkocnv  20829  submtmd  21119  prdsdsf  21382  ressprdsds  21386  blfvalps  21398  prdsxmslem2  21544  tmsxpsval  21553  ngpds  21617  subgngp  21643  tngngp  21662  isnlm  21678  lssnlm  21703  isphtpy  22012  isphtpc  22025  pi1cpbl  22075  pi1addf  22078  pi1addval  22079  pi1grplem  22080  clmsub  22111  clmvsass  22118  clmvsdir  22119  cvsdiv  22140  iscph  22148  cphdir  22182  cphdi  22183  cph2di  22184  cph2subdi  22187  cphass  22188  tchval  22192  ipcau2  22208  tchcphlem1  22209  tchcphlem2  22210  caufval  22245  rrxip  22349  dvlip2  22947  q1pval  23104  r1pval  23107  dvntaylp  23326  efabl  23499  efsubm  23500  dchrmul  24176  istrkgc  24502  istrkgb  24503  istrkgcb  24504  istrkge  24505  istrkgl  24506  istrkgld  24507  iscgrg  24557  isismt  24579  tglngval  24596  legval  24629  ishlg  24647  mirval  24700  israg  24742  ishpg  24801  lmif  24827  islmib  24829  isinag  24879  ttgval  24905  wlkon  25261  trlon  25270  trlonprop  25272  pthon  25305  pthonprop  25307  spthon  25312  spthonprp  25315  isconngra  25400  isconngra1  25401  is2wlkonot  25591  is2spthonot  25592  2wlkonot  25593  2spthonot  25594  2wlksot  25595  2spthsot  25596  2wlkonot3v  25603  2spthonot3v  25604  grpodivval  25971  gxval  25986  subgoov  26033  isrngo  26106  vcoprne  26198  dipfval  26338  ipval  26339  sspgval  26368  sspsval  26370  lnoval  26393  ajfval  26450  dipdir  26483  dipass  26486  htth  26571  isomnd  28464  submomnd  28473  inftmrel  28497  isinftm  28498  isslmd  28518  rngurd  28551  rdivmuldivd  28554  isorng  28562  suborng  28578  resv1r  28600  smatlem  28623  submatminr1  28636  metidval  28693  pstmval  28698  pstmfval  28699  zlm0  28766  zlm1  28767  sitmval  29182  istrkg2d  29483  afsval  29488  mclsrcl  30199  mppsval  30210  istotbnd  32101  isbnd  32112  rrnequiv  32167  rngohomval  32203  idlval  32246  pridlval  32266  lflset  32625  islfld  32628  ldualvadd  32695  ldualsmul  32701  ldualvs  32703  isopos  32746  cmtfvalN  32776  iscvlat  32889  ishlat1  32918  lineset  33303  psubspset  33309  paddfval  33362  paddval  33363  ltrnfset  33682  trnfsetN  33721  trlfset  33726  tgrpov  34315  erngplus  34370  erngmul  34373  erngplus-rN  34378  erngmul-rN  34381  erngdvlem3  34557  erngdvlem4  34558  erng0g  34561  erngdvlem3-rN  34565  erngdvlem4-rN  34566  dvaplusg  34576  dvamulr  34579  dvavadd  34582  dvavsca  34584  dvalveclem  34593  dvhmulr  34654  dvhfvadd  34659  dvhvadd  34660  dvhopvadd2  34662  dvhvaddcl  34663  dvhvaddcomN  34664  dvhvsca  34669  dvhlveclem  34676  dvh0g  34679  djavalN  34703  diblsmopel  34739  dicvaddcl  34758  cdlemn6  34770  dihffval  34798  dihopelvalcpre  34816  djhval  34966  lcdvaddval  35166  lcdsmul  35170  lcdvsval  35172  lcdlkreq2N  35191  hvmapffval  35326  hvmapfval  35327  hdmap1fval  35365  hgmapffval  35456  hgmapfval  35457  hgmapadd  35465  hlhilipval  35520  hlhilhillem  35531  hoidmvval0b  38412  hoidmvlelem2  38418  hoidmvlelem3  38419  hoidmvle  38422  ovnhoi  38425  hoiqssbl  38447  hspmbllem2  38449  mptmpt2opabbrd  39034  mptmpt2opabovd  39035  1wlksonproplem  39675  ismgmd  39829  ismgmhm  39836  issubmgm  39842  resmgmhm  39851  resmgmhm2  39852  resmgmhm2b  39853  idfusubc  39919  rnghmval  39944  lidlmsgrp  39979  lidlrng  39980  zlidlring  39981  uzlidlring  39982  rnghmresel  40019  rngchom  40022  rngcco  40026  rnghmsubcsetclem1  40030  rhmresel  40065  ringchom  40068  ringcco  40072  rhmsubcsetclem1  40076  rhmsubcrngclem1  40082  irinitoringc  40124  ovmpt2rdxf  40173  lincop  40254  lincval  40255  lincsum  40275  lincscm  40276  lmod1lem2  40334  lmod1lem3  40335  lmod1lem4  40336  ldepsnlinc  40354