Theorem oveqd 5891

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 5880	. 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 1353  (class class class)co 5874

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  oveq123d  5895  oveqdr  5902  csbov12g  5913  ovmpodxf  5999  oprssov  6015  ofeq  6084  fnmpoovd  6215  seqeq2  10448  prdsex  12717  imasex  12725  imasival  12726  plusffvalg  12780  mgm1  12788  grpidvalg  12791  grpidd  12801  sgrp1  12815  ismndd  12837  issubmnd  12842  mnd1  12846  ismhm  12852  issubm  12862  isgrp  12882  isgrpd2e  12895  grpidd2  12913  grpinvfvalg  12914  grp1  12975  subg0  13038  subginv  13039  subgcl  13042  issubgrpd2  13048  isnsg  13060  nmznsg  13071  iscmn  13094  iscmnd  13099  dfur2g  13143  issrg  13146  srgcl  13151  srgass  13152  srgideu  13153  issrgid  13162  srgpcomp  13171  srgpcompp  13172  isring  13181  ringcl  13194  crngcom  13195  iscrng2  13196  ringass  13197  ringideu  13198  isringid  13206  ringidss  13210  ringpropd  13215  ring1  13234  opprmulg  13241  oppr0g  13249  oppr1g  13250  opprnegg  13251  mulgass3  13252  reldvdsrsrg  13259  dvdsrvald  13260  dvdsrd  13261  opprunitd  13277  dvrvald  13301  rdivmuldivd  13311  islring  13331  lringuplu  13335  subrg1  13350  subrgmcl  13352  subrgdvds  13354  subrguss  13355  subrginv  13356  subrgdv  13357  subrgunit  13358  subrgugrp  13359  issubrg3  13366  aprval  13370  aprap  13374  islmod  13379  islmodd  13381  scaffvalg  13394  blfvalps  13855