Theorem oveqd 6099

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 6088	. 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 1364  (class class class)co 6082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2713  df-uni 4082  df-br 4283  df-iota 5371  df-fv 5416  df-ov 6085

This theorem is referenced by:  oveq123d  6103  csbov  6114  csbov12g  6116  ovmpt2dxf  6207  oprssov  6223  ofeq  6313  fnmpt2ovd  6642  ruclem1  13498  vdwapval  14019  vdwapid1  14021  vdwmc2  14025  vdwpc  14026  vdwlem5  14031  vdwlem8  14034  vdwlem13  14039  prdsval  14378  prdsdsval2  14407  pwsplusgval  14413  pwsmulrval  14414  pwsvscafval  14417  imasval  14434  iscat  14595  iscatd  14596  catidex  14597  catideu  14598  cidfval  14599  cidval  14600  catidd  14603  iscatd2  14604  catlid  14606  catrid  14607  proplem3  14614  homffval  14615  homfeqd  14619  homfeqval  14621  comfffval  14622  comffval  14623  comfeq  14630  comfeqd  14631  comfeqval  14632  catpropd  14633  oppcval  14637  oppcco  14641  monfval  14656  ismon  14657  oppcmon  14662  oppcepi  14663  sectffval  14674  sectfval  14675  invffval  14681  isoval  14688  issubc  14733  issubc3  14744  isfunc  14759  cofuval  14777  cofuval2  14782  funcres  14791  funcres2b  14792  funcres2  14793  funcres2c  14796  isfull  14805  isfth  14809  fullres2c  14834  natfval  14841  isnat  14842  fucval  14853  fucco  14857  fucpropd  14872  homarcl  14881  coafval  14917  resssetc  14945  resscatc  14958  catciso  14960  xpcval  14972  1stfval  14986  2ndfval  14989  prfval  14994  prfcl  14998  evlfval  15012  curfval  15018  curf1cl  15023  curfcl  15027  uncf1  15031  uncf2  15032  diag12  15039  diag2  15040  curf2ndf  15042  hofval  15047  hof1  15049  hof2fval  15050  hofcl  15054  yon12  15060  yon2  15061  hofpropd  15062  joinval  15160  meetval  15174  isdlat  15348  ismnd  15402  plusffval  15412  grpidval  15417  grpidd  15428  ismndd  15429  issubmnd  15434  submnd0  15436  ismhm  15451  issubm  15459  resmhm  15471  resmhm2  15472  resmhm2b  15473  gsumvalx  15486  gsumpropd  15488  gsumress  15489  isgrp  15531  isgrpd2e  15542  grpidd2  15557  grpinvfval  15558  imasgrp2  15652  imasgrp  15653  subg0  15669  subginv  15670  subgcl  15673  issubgrpd2  15679  isnsg  15692  isghm  15729  resghm  15745  isga  15791  subgga  15800  gasubg  15802  cntzfval  15820  resscntz  15831  odfval  16018  gexval  16059  lsmfval  16119  lsmvalx  16120  oppglsm  16123  subglsm  16152  pj1fval  16173  efgtval  16202  iscmn  16266  iscmnd  16271  submcmn2  16305  iscyg  16338  isrng  16587  rngidss  16609  prdsmgp  16639  mulgass3  16665  dvdsrval  16673  isirred  16727  isdrngd  16783  isdrngrd  16784  subrg1  16801  subrgmcl  16803  subrgdvds  16805  subrguss  16806  subrginv  16807  subrgdv  16808  subrgunit  16809  subrgugrp  16810  abvfval  16829  isabvd  16831  issrngd  16872  islmod  16878  islmodd  16880  scaffval  16892  lmodpropd  16934  lssset  16939  islssd  16941  prdslmodd  16974  islmhm  17032  reslmhm  17057  reslmhm2  17058  reslmhm2b  17059  islbs  17081  rlmvneg  17212  rrgval  17282  isassa  17311  isassad  17318  psrval  17365  resspsradd  17424  resspsrmul  17425  resspsrvsca  17426  mplmon2mul  17517  ply1coe  17645  isphl  17901  ipffval  17921  isphld  17927  ocvfval  17935  isobs  17989  frlmplusgval  18035  frlmsubgval  18036  frlmvscafval  18037  frlmip  18047  frlmipval  18048  frlmup1  18070  lsslindf  18103  mamufval  18127  matplusg2  18171  matvsca2  18172  mat1  18178  mattposm  18188  mvmulfval  18197  ma1repveval  18226  mdetrlin  18253  mdetrsca  18254  mdetmul  18273  madurid  18294  minmar1cl  18301  smadiadetglem1  18321  smadiadetr  18325  matinv  18327  slesolinv  18330  slesolinvbi  18331  cramerimplem3  18335  xkocnv  19231  submtmd  19519  prdsdsf  19786  ressprdsds  19790  blfvalps  19802  prdsxmslem2  19948  tmsxpsval  19957  ngpds  20039  subgngp  20065  tngngp  20084  isnlm  20100  lssnlm  20125  isphtpy  20397  isphtpc  20410  pi1cpbl  20460  pi1addf  20463  pi1addval  20464  pi1grplem  20465  clmsub  20496  clmvsass  20503  clmvsdir  20504  cvsdiv  20525  iscph  20533  cphdir  20567  cphdi  20568  cph2di  20569  cph2subdi  20572  cphass  20573  tchval  20577  ipcau2  20593  tchcphlem1  20594  tchcphlem2  20595  caufval  20630  rrxip  20738  dvlip2  21311  evl1expd  21391  q1pval  21512  r1pval  21515  dvntaylp  21723  dchrmul  22474  istrkgc  22804  istrkgb  22805  istrkgcb  22806  istrkge  22807  istrkgl  22808  istrkg2d  22809  iscgrg  22848  tglngval  22866  legval  22893  mirval  22927  ttgval  22946  wlkon  23254  trlon  23264  trlonprop  23266  pthon  23299  pthonprop  23301  spthon  23306  spthonprp  23309  isconngra  23383  isconngra1  23384  grpodivval  23555  gxval  23570  subgoov  23617  isrngo  23690  vcoprne  23782  dipfval  23922  ipval  23923  sspgval  23952  sspsval  23954  lnoval  23977  ajfval  24034  dipdir  24067  dipass  24070  htth  24145  isomnd  25990  submomnd  25999  inftmrel  26023  isinftm  26024  issrg  26044  isslmd  26069  rngurd  26111  rdivmuldivd  26114  isorng  26122  suborng  26138  resv0g  26160  resv1r  26161  resvcmn  26162  metidval  26173  pstmval  26178  pstmfval  26179  zlm0  26247  zlm1  26248  sitmval  26584  afsval  26845  istotbnd  28514  isbnd  28525  rrnequiv  28580  rngohomval  28616  idlval  28659  pridlval  28679  is2wlkonot  30230  is2spthonot  30231  2wlkonot  30232  2spthonot  30233  2wlksot  30234  2spthsot  30235  2wlkonot3v  30242  2spthonot3v  30243  ovmpt2rdxf  30576  matplusgcell  30651  matsubgcell  30652  matvscacell  30653  mat1dimmul  30663  dmatmul  30667  dmatcrng  30672  scmatcrng  30679  lincop  30691  lincval  30692  lincsum  30712  lincscm  30713  lmod1lem1  30778  lmod1lem2  30779  lmod1lem3  30780  lmod1lem4  30781  lmod1lem5  30782  ldepsnlinc  30799  lflset  32317  islfld  32320  ldualvadd  32387  ldualsmul  32393  ldualvs  32395  isopos  32438  cmtfvalN  32468  iscvlat  32581  ishlat1  32610  lineset  32995  psubspset  33001  paddfval  33054  paddval  33055  ltrnfset  33374  trnfsetN  33412  trlfset  33417  tgrpov  34005  erngplus  34060  erngmul  34063  erngplus-rN  34068  erngmul-rN  34071  erngdvlem3  34247  erngdvlem4  34248  erng0g  34251  erngdvlem3-rN  34255  erngdvlem4-rN  34256  dvaplusg  34266  dvamulr  34269  dvavadd  34272  dvavsca  34274  dvalveclem  34283  dvhmulr  34344  dvhfvadd  34349  dvhvadd  34350  dvhopvadd2  34352  dvhvaddcl  34353  dvhvaddcomN  34354  dvhvsca  34359  dvhlveclem  34366  dvh0g  34369  djavalN  34393  diblsmopel  34429  dicvaddcl  34448  cdlemn6  34460  dihffval  34488  dihopelvalcpre  34506  djhval  34656  lcdvaddval  34856  lcdsmul  34860  lcdvsval  34862  lcdlkreq2N  34881  hvmapffval  35016  hvmapfval  35017  hdmap1fval  35055  hgmapffval  35146  hgmapfval  35147  hgmapadd  35155  hlhilipval  35210  hlhilhillem  35221