Theorem oveqd 6069

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 6058	. 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 1398  (class class class)co 6052

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055

This theorem is referenced by:  oveq123d  6073  oveqdr  6080  csbov12g  6092  ovmpodxf  6181  oprssov  6198  ofeqd  6270  ofeq  6271  fnmpoovd  6413  seqeq2  10817  prdsex  13499  prdsval  13503  pwsplusgval  13525  pwsmulrval  13526  imasex  13535  imasival  13536  plusffvalg  13592  mgm1  13600  grpidvalg  13603  grpidd  13613  gsumress  13625  sgrp1  13641  issgrpd  13642  ismndd  13667  issubmnd  13672  mnd1  13685  ismhm  13691  mhmex  13692  issubm  13702  resmhm  13717  resmhm2  13718  resmhm2b  13719  isgrp  13736  isgrpd2e  13750  grpidd2  13771  grpinvfvalg  13772  grp1  13836  imasgrp2  13844  imasgrp  13845  subg0  13914  subginv  13915  subgcl  13918  issubgrpd2  13924  isnsg  13936  nmznsg  13947  isghm  13977  resghm  13994  iscmn  14027  iscmnd  14032  imasabl  14070  rngass  14100  rngcl  14105  rngpropd  14116  dfur2g  14123  issrg  14126  srgcl  14131  srgass  14132  srgideu  14133  issrgid  14142  srgpcomp  14151  srgpcompp  14152  isring  14161  ringcl  14174  crngcom  14175  iscrng2  14176  ringass  14177  ringideu  14178  isringid  14186  ringidss  14190  ringpropd  14199  ring1  14220  opprmulg  14232  oppr0g  14242  oppr1g  14243  opprnegg  14244  mulgass3  14246  dvdsrvald  14255  dvdsrd  14256  opprunitd  14272  dvrvald  14296  rdivmuldivd  14306  rhmmul  14326  isrhm2d  14327  rhmopp  14338  rhmunitinv  14340  islring  14354  lringuplu  14358  subrngmcl  14371  subrg1  14393  subrgmcl  14395  subrgdvds  14397  subrguss  14398  subrginv  14399  subrgdv  14400  subrgunit  14401  subrgugrp  14402  issubrg3  14409  rhmpropd  14416  rrgval  14424  aprval  14445  aprap  14449  islmod  14456  islmodd  14458  scaffvalg  14471  lmodpropd  14514  lsssetm  14521  islssmd  14524  islidlm  14644  lidlacl  14649  rnglidlmmgm  14661  rnglidlmsgrp  14662  rnglidlrng  14663  rspsn  14699  psrval  14831  psradd  14851  mpladd  14876  blfvalps  15267  lgseisenlem3  15962  lgseisenlem4  15963