Theorem oveqd 6024

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

Syntax hints:   -> wi 4   = wceq 1395  (class class class)co 6007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  oveq123d  6028  oveqdr  6035  csbov12g  6047  ovmpodxf  6136  oprssov  6153  ofeqd  6226  ofeq  6227  fnmpoovd  6367  seqeq2  10681  prdsex  13310  prdsval  13314  pwsplusgval  13336  pwsmulrval  13337  imasex  13346  imasival  13347  plusffvalg  13403  mgm1  13411  grpidvalg  13414  grpidd  13424  gsumress  13436  sgrp1  13452  issgrpd  13453  ismndd  13478  issubmnd  13483  mnd1  13496  ismhm  13502  mhmex  13503  issubm  13513  resmhm  13528  resmhm2  13529  resmhm2b  13530  isgrp  13547  isgrpd2e  13561  grpidd2  13582  grpinvfvalg  13583  grp1  13647  imasgrp2  13655  imasgrp  13656  subg0  13725  subginv  13726  subgcl  13729  issubgrpd2  13735  isnsg  13747  nmznsg  13758  isghm  13788  resghm  13805  iscmn  13838  iscmnd  13843  imasabl  13881  rngass  13910  rngcl  13915  rngpropd  13926  dfur2g  13933  issrg  13936  srgcl  13941  srgass  13942  srgideu  13943  issrgid  13952  srgpcomp  13961  srgpcompp  13962  isring  13971  ringcl  13984  crngcom  13985  iscrng2  13986  ringass  13987  ringideu  13988  isringid  13996  ringidss  14000  ringpropd  14009  ring1  14030  opprmulg  14042  oppr0g  14052  oppr1g  14053  opprnegg  14054  mulgass3  14056  dvdsrvald  14065  dvdsrd  14066  opprunitd  14082  dvrvald  14106  rdivmuldivd  14116  rhmmul  14136  isrhm2d  14137  rhmopp  14148  rhmunitinv  14150  islring  14164  lringuplu  14168  subrngmcl  14181  subrg1  14203  subrgmcl  14205  subrgdvds  14207  subrguss  14208  subrginv  14209  subrgdv  14210  subrgunit  14211  subrgugrp  14212  issubrg3  14219  rhmpropd  14226  rrgval  14234  aprval  14254  aprap  14258  islmod  14263  islmodd  14265  scaffvalg  14278  lmodpropd  14321  lsssetm  14328  islssmd  14331  islidlm  14451  lidlacl  14456  rnglidlmmgm  14468  rnglidlmsgrp  14469  rnglidlrng  14470  rspsn  14506  psrval  14638  psradd  14651  mpladd  14676  blfvalps  15067  lgseisenlem3  15759  lgseisenlem4  15760