Theorem oveqd 5914

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 5903	. 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 1364  (class class class)co 5897

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5900

This theorem is referenced by:  oveq123d  5918  oveqdr  5925  csbov12g  5936  ovmpodxf  6023  oprssov  6039  ofeqd  6109  ofeq  6110  fnmpoovd  6241  seqeq2  10482  prdsex  12777  imasex  12785  imasival  12786  plusffvalg  12841  mgm1  12849  grpidvalg  12852  grpidd  12862  gsumress  12873  sgrp1  12889  issgrpd  12890  ismndd  12913  issubmnd  12918  mnd1  12922  ismhm  12928  mhmex  12929  issubm  12939  resmhm  12954  resmhm2  12955  resmhm2b  12956  isgrp  12966  isgrpd2e  12980  grpidd2  13000  grpinvfvalg  13001  grp1  13065  imasgrp2  13067  imasgrp  13068  subg0  13136  subginv  13137  subgcl  13140  issubgrpd2  13146  isnsg  13158  nmznsg  13169  isghm  13199  resghm  13216  iscmn  13249  iscmnd  13254  imasabl  13290  rngass  13310  rngcl  13315  rngpropd  13326  dfur2g  13333  issrg  13336  srgcl  13341  srgass  13342  srgideu  13343  issrgid  13352  srgpcomp  13361  srgpcompp  13362  isring  13371  ringcl  13384  crngcom  13385  iscrng2  13386  ringass  13387  ringideu  13388  isringid  13396  ringidss  13400  ringpropd  13409  ring1  13428  opprmulg  13438  oppr0g  13448  oppr1g  13449  opprnegg  13450  mulgass3  13452  reldvdsrsrg  13459  dvdsrvald  13460  dvdsrd  13461  opprunitd  13477  dvrvald  13501  rdivmuldivd  13511  rhmmul  13531  isrhm2d  13532  rhmopp  13543  rhmunitinv  13545  islring  13556  lringuplu  13560  subrngmcl  13573  subrg1  13595  subrgmcl  13597  subrgdvds  13599  subrguss  13600  subrginv  13601  subrgdv  13602  subrgunit  13603  subrgugrp  13604  issubrg3  13611  aprval  13615  aprap  13619  islmod  13624  islmodd  13626  scaffvalg  13639  lmodpropd  13682  lsssetm  13689  islssmd  13692  islidlm  13812  lidlacl  13817  rnglidlmmgm  13829  rnglidlmsgrp  13830  rnglidlrng  13831  psrval  13961  psradd  13972  blfvalps  14362