Theorem oveqd 5935

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 5924	. 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 5918

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  oveq123d  5939  oveqdr  5946  csbov12g  5957  ovmpodxf  6044  oprssov  6060  ofeqd  6132  ofeq  6133  fnmpoovd  6268  seqeq2  10522  prdsex  12880  imasex  12888  imasival  12889  plusffvalg  12945  mgm1  12953  grpidvalg  12956  grpidd  12966  gsumress  12978  sgrp1  12994  issgrpd  12995  ismndd  13018  issubmnd  13023  mnd1  13027  ismhm  13033  mhmex  13034  issubm  13044  resmhm  13059  resmhm2  13060  resmhm2b  13061  isgrp  13078  isgrpd2e  13092  grpidd2  13113  grpinvfvalg  13114  grp1  13178  imasgrp2  13180  imasgrp  13181  subg0  13250  subginv  13251  subgcl  13254  issubgrpd2  13260  isnsg  13272  nmznsg  13283  isghm  13313  resghm  13330  iscmn  13363  iscmnd  13368  imasabl  13406  rngass  13435  rngcl  13440  rngpropd  13451  dfur2g  13458  issrg  13461  srgcl  13466  srgass  13467  srgideu  13468  issrgid  13477  srgpcomp  13486  srgpcompp  13487  isring  13496  ringcl  13509  crngcom  13510  iscrng2  13511  ringass  13512  ringideu  13513  isringid  13521  ringidss  13525  ringpropd  13534  ring1  13555  opprmulg  13567  oppr0g  13577  oppr1g  13578  opprnegg  13579  mulgass3  13581  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrd  13590  opprunitd  13606  dvrvald  13630  rdivmuldivd  13640  rhmmul  13660  isrhm2d  13661  rhmopp  13672  rhmunitinv  13674  islring  13688  lringuplu  13692  subrngmcl  13705  subrg1  13727  subrgmcl  13729  subrgdvds  13731  subrguss  13732  subrginv  13733  subrgdv  13734  subrgunit  13735  subrgugrp  13736  issubrg3  13743  rhmpropd  13750  rrgval  13758  aprval  13778  aprap  13782  islmod  13787  islmodd  13789  scaffvalg  13802  lmodpropd  13845  lsssetm  13852  islssmd  13855  islidlm  13975  lidlacl  13980  rnglidlmmgm  13992  rnglidlmsgrp  13993  rnglidlrng  13994  rspsn  14030  psrval  14152  psradd  14163  blfvalps  14553  lgseisenlem3  15188  lgseisenlem4  15189