Theorem oveqd 6030

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 6019	. 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 6013

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 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  oveq123d  6034  oveqdr  6041  csbov12g  6053  ovmpodxf  6142  oprssov  6159  ofeqd  6232  ofeq  6233  fnmpoovd  6375  seqeq2  10703  prdsex  13342  prdsval  13346  pwsplusgval  13368  pwsmulrval  13369  imasex  13378  imasival  13379  plusffvalg  13435  mgm1  13443  grpidvalg  13446  grpidd  13456  gsumress  13468  sgrp1  13484  issgrpd  13485  ismndd  13510  issubmnd  13515  mnd1  13528  ismhm  13534  mhmex  13535  issubm  13545  resmhm  13560  resmhm2  13561  resmhm2b  13562  isgrp  13579  isgrpd2e  13593  grpidd2  13614  grpinvfvalg  13615  grp1  13679  imasgrp2  13687  imasgrp  13688  subg0  13757  subginv  13758  subgcl  13761  issubgrpd2  13767  isnsg  13779  nmznsg  13790  isghm  13820  resghm  13837  iscmn  13870  iscmnd  13875  imasabl  13913  rngass  13942  rngcl  13947  rngpropd  13958  dfur2g  13965  issrg  13968  srgcl  13973  srgass  13974  srgideu  13975  issrgid  13984  srgpcomp  13993  srgpcompp  13994  isring  14003  ringcl  14016  crngcom  14017  iscrng2  14018  ringass  14019  ringideu  14020  isringid  14028  ringidss  14032  ringpropd  14041  ring1  14062  opprmulg  14074  oppr0g  14084  oppr1g  14085  opprnegg  14086  mulgass3  14088  dvdsrvald  14097  dvdsrd  14098  opprunitd  14114  dvrvald  14138  rdivmuldivd  14148  rhmmul  14168  isrhm2d  14169  rhmopp  14180  rhmunitinv  14182  islring  14196  lringuplu  14200  subrngmcl  14213  subrg1  14235  subrgmcl  14237  subrgdvds  14239  subrguss  14240  subrginv  14241  subrgdv  14242  subrgunit  14243  subrgugrp  14244  issubrg3  14251  rhmpropd  14258  rrgval  14266  aprval  14286  aprap  14290  islmod  14295  islmodd  14297  scaffvalg  14310  lmodpropd  14353  lsssetm  14360  islssmd  14363  islidlm  14483  lidlacl  14488  rnglidlmmgm  14500  rnglidlmsgrp  14501  rnglidlrng  14502  rspsn  14538  psrval  14670  psradd  14683  mpladd  14708  blfvalps  15099  lgseisenlem3  15791  lgseisenlem4  15792