Theorem oveqd 6216

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 6205	. 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 1370  (class class class)co 6199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2804  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202

This theorem is referenced by:  oveq123d  6220  csbov  6231  csbov12g  6233  ovmpt2dxf  6325  oprssov  6341  ofeq  6431  fnmpt2ovd  6760  ruclem1  13630  vdwapval  14151  vdwapid1  14153  vdwmc2  14157  vdwpc  14158  vdwlem5  14163  vdwlem8  14166  vdwlem13  14171  prdsval  14511  prdsdsval2  14540  pwsplusgval  14546  pwsmulrval  14547  pwsvscafval  14550  imasval  14567  iscat  14728  iscatd  14729  catidex  14730  catideu  14731  cidfval  14732  cidval  14733  catidd  14736  iscatd2  14737  catlid  14739  catrid  14740  proplem3  14747  homffval  14748  homfeqd  14752  homfeqval  14754  comfffval  14755  comffval  14756  comfeq  14763  comfeqd  14764  comfeqval  14765  catpropd  14766  oppcval  14770  oppcco  14774  monfval  14789  ismon  14790  oppcmon  14795  oppcepi  14796  sectffval  14807  sectfval  14808  invffval  14814  isoval  14821  issubc  14866  issubc3  14877  isfunc  14892  cofuval  14910  cofuval2  14915  funcres  14924  funcres2b  14925  funcres2  14926  funcres2c  14929  isfull  14938  isfth  14942  fullres2c  14967  natfval  14974  isnat  14975  fucval  14986  fucco  14990  fucpropd  15005  homarcl  15014  coafval  15050  resssetc  15078  resscatc  15091  catciso  15093  xpcval  15105  1stfval  15119  2ndfval  15122  prfval  15127  prfcl  15131  evlfval  15145  curfval  15151  curf1cl  15156  curfcl  15160  uncf1  15164  uncf2  15165  diag12  15172  diag2  15173  curf2ndf  15175  hofval  15180  hof1  15182  hof2fval  15183  hofcl  15187  yon12  15193  yon2  15194  hofpropd  15195  joinval  15293  meetval  15307  isdlat  15481  ismnd  15535  plusffval  15545  grpidval  15550  grpidd  15561  ismndd  15562  issubmnd  15567  submnd0  15569  ismhm  15584  issubm  15593  resmhm  15605  resmhm2  15606  resmhm2b  15607  gsumvalx  15620  gsumpropd  15622  gsumress  15625  isgrp  15667  isgrpd2e  15678  grpidd2  15693  grpinvfval  15694  imasgrp2  15788  imasgrp  15789  subg0  15805  subginv  15806  subgcl  15809  issubgrpd2  15815  isnsg  15828  isghm  15865  resghm  15881  isga  15927  subgga  15936  gasubg  15938  cntzfval  15956  resscntz  15967  odfval  16156  gexval  16197  lsmfval  16257  lsmvalx  16258  oppglsm  16261  subglsm  16290  pj1fval  16311  efgtval  16340  iscmn  16404  iscmnd  16409  submcmn2  16443  iscyg  16476  issrg  16730  isrng  16771  rngidss  16793  prdsmgp  16824  mulgass3  16851  dvdsrval  16859  isirred  16913  isdrngd  16979  isdrngrd  16980  subrg1  16997  subrgmcl  16999  subrgdvds  17001  subrguss  17002  subrginv  17003  subrgdv  17004  subrgunit  17005  subrgugrp  17006  abvfval  17025  isabvd  17027  issrngd  17068  islmod  17074  islmodd  17076  scaffval  17088  lmodpropd  17130  lssset  17137  islssd  17139  prdslmodd  17172  islmhm  17230  reslmhm  17255  reslmhm2  17256  reslmhm2b  17257  islbs  17279  rlmvneg  17410  rrgval  17480  isassa  17509  isassad  17516  psrval  17551  resspsradd  17611  resspsrmul  17612  resspsrvsca  17613  mplmon2mul  17706  ply1coe  17870  ply1coeOLD  17871  evl1expd  17903  evl1scvarpw  17921  isphl  18181  ipffval  18201  isphld  18207  ocvfval  18215  isobs  18269  frlmplusgval  18315  frlmsubgval  18316  frlmvscafval  18317  frlmip  18327  frlmipval  18328  frlmup1  18350  lsslindf  18383  mamufval  18407  matplusg2  18452  matvsca2  18453  mat1  18460  mattposm  18470  mvmulfval  18479  ma1repveval  18508  mdetrlin  18539  mdetrsca  18540  mdetmul  18560  madurid  18581  minmar1cl  18588  smadiadetglem1  18608  smadiadetr  18612  matinv  18614  slesolinv  18617  slesolinvbi  18618  cramerimplem3  18622  xkocnv  19518  submtmd  19806  prdsdsf  20073  ressprdsds  20077  blfvalps  20089  prdsxmslem2  20235  tmsxpsval  20244  ngpds  20326  subgngp  20352  tngngp  20371  isnlm  20387  lssnlm  20412  isphtpy  20684  isphtpc  20697  pi1cpbl  20747  pi1addf  20750  pi1addval  20751  pi1grplem  20752  clmsub  20783  clmvsass  20790  clmvsdir  20791  cvsdiv  20812  iscph  20820  cphdir  20854  cphdi  20855  cph2di  20856  cph2subdi  20859  cphass  20860  tchval  20864  ipcau2  20880  tchcphlem1  20881  tchcphlem2  20882  caufval  20917  rrxip  21025  dvlip2  21599  q1pval  21757  r1pval  21760  dvntaylp  21968  dchrmul  22719  istrkgc  23047  istrkgb  23048  istrkgcb  23049  istrkge  23050  istrkgl  23051  istrkg2d  23052  istrkgld  23053  iscgrg  23100  tglngval  23120  legval  23152  mirval  23201  israg  23233  ttgval  23272  wlkon  23580  trlon  23590  trlonprop  23592  pthon  23625  pthonprop  23627  spthon  23632  spthonprp  23635  isconngra  23709  isconngra1  23710  grpodivval  23881  gxval  23896  subgoov  23943  isrngo  24016  vcoprne  24108  dipfval  24248  ipval  24249  sspgval  24278  sspsval  24280  lnoval  24303  ajfval  24360  dipdir  24393  dipass  24396  htth  24471  isomnd  26308  submomnd  26317  inftmrel  26341  isinftm  26342  isslmd  26362  rngurd  26400  rdivmuldivd  26403  isorng  26411  suborng  26427  resv0g  26448  resv1r  26449  resvcmn  26450  metidval  26461  pstmval  26466  pstmfval  26467  zlm0  26535  zlm1  26536  sitmval  26877  afsval  27138  istotbnd  28815  isbnd  28826  rrnequiv  28881  rngohomval  28917  idlval  28960  pridlval  28980  is2wlkonot  30529  is2spthonot  30530  2wlkonot  30531  2spthonot  30532  2wlksot  30533  2spthsot  30534  2wlkonot3v  30541  2spthonot3v  30542  ovmpt2rdxf  30876  assamulgscmlem2  30975  lply1binomsc  31009  matplusgcell  31016  matsubgcell  31017  matinvgcell  31018  matmulcell  31019  matvscacell  31020  mpt2matmul  31027  mat1dimmul  31037  dmatmul  31041  dmatcrng  31046  scmatcrng  31053  lincop  31060  lincval  31061  lincsum  31081  lincscm  31082  lmod1lem1  31147  lmod1lem2  31148  lmod1lem3  31149  lmod1lem4  31150  lmod1lem5  31151  ldepsnlinc  31168  cpmatacl  31191  mat2pmatghm  31205  decpmatmullem  31244  decpmatmul  31245  pmatcollpw1lem1  31247  pmatcollpw2lem  31250  pmatcollpwlem  31253  pmatcollpw3  31256  pmatcollpw3fi  31257  mply1topmatval  31276  mp2pm2mplem1  31278  mp2pm2mplem4  31281  mp2pm2mplem5  31282  mp2pm2mp  31283  cpmat1d  31307  cpscmatgsummon  31316  chfacfpmmulgsum2  31336  lflset  33027  islfld  33030  ldualvadd  33097  ldualsmul  33103  ldualvs  33105  isopos  33148  cmtfvalN  33178  iscvlat  33291  ishlat1  33320  lineset  33705  psubspset  33711  paddfval  33764  paddval  33765  ltrnfset  34084  trnfsetN  34122  trlfset  34127  tgrpov  34715  erngplus  34770  erngmul  34773  erngplus-rN  34778  erngmul-rN  34781  erngdvlem3  34957  erngdvlem4  34958  erng0g  34961  erngdvlem3-rN  34965  erngdvlem4-rN  34966  dvaplusg  34976  dvamulr  34979  dvavadd  34982  dvavsca  34984  dvalveclem  34993  dvhmulr  35054  dvhfvadd  35059  dvhvadd  35060  dvhopvadd2  35062  dvhvaddcl  35063  dvhvaddcomN  35064  dvhvsca  35069  dvhlveclem  35076  dvh0g  35079  djavalN  35103  diblsmopel  35139  dicvaddcl  35158  cdlemn6  35170  dihffval  35198  dihopelvalcpre  35216  djhval  35366  lcdvaddval  35566  lcdsmul  35570  lcdvsval  35572  lcdlkreq2N  35591  hvmapffval  35726  hvmapfval  35727  hdmap1fval  35765  hgmapffval  35856  hgmapfval  35857  hgmapadd  35865  hlhilipval  35920  hlhilhillem  35931