Theorem oveqd 6075

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 6064	. 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 6058

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 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  oveq123d  6079  oveqdr  6086  csbov12g  6098  ovmpodxf  6187  oprssov  6204  ofeqd  6277  ofeq  6278  fnmpoovd  6424  seqeq2  10837  imasex  13569  imasival  13570  plusffvalg  13625  mgm1  13633  grpidvalg  13636  grpidd  13646  gsumress  13658  sgrp1  13674  issgrpd  13675  ismndd  13698  issubmnd  13703  mnd1  13710  ismhm  13716  mhmex  13717  issubm  13727  resmhm  13742  resmhm2  13743  resmhm2b  13744  isgrp  13761  isgrpd2e  13775  grpidd2  13796  grpinvfvalg  13797  grp1  13861  imasgrp2  13863  imasgrp  13864  subg0  13933  subginv  13934  subgcl  13937  issubgrpd2  13943  isnsg  13955  nmznsg  13966  isghm  13996  resghm  14013  iscmn  14046  iscmnd  14051  imasabl  14089  prdsex  14114  prdsval  14115  pwsplusgval  14150  pwsmulrval  14151  rngass  14178  rngcl  14183  rngpropd  14194  dfur2g  14205  issrg  14208  srgcl  14213  srgass  14214  srgideu  14215  issrgid  14224  srgpcomp  14233  srgpcompp  14234  isring  14243  ringcl  14256  crngcom  14257  iscrng2  14258  ringass  14259  ringideu  14260  isringid  14268  ringidss  14272  ringpropd  14281  ring1  14302  opprmulg  14314  oppr0g  14325  oppr1g  14326  opprnegg  14327  mulgass3  14329  dvdsrvald  14338  dvdsrd  14339  opprunitd  14355  dvrvald  14379  rdivmuldivd  14389  rhmmul  14409  isrhm2d  14410  rhmopp  14421  rhmunitinv  14423  islring  14437  lringuplu  14441  opprlring  14442  subrngmcl  14455  subrg1  14477  subrgmcl  14479  subrgdvds  14481  subrguss  14482  subrginv  14483  subrgdv  14484  subrgunit  14485  subrgugrp  14486  issubrg3  14493  rhmpropd  14500  rrgval  14508  aprval  14529  aprap  14536  aprprop  14539  islmod  14565  islmodd  14567  scaffvalg  14580  lmodpropd  14623  lsssetm  14630  islssmd  14633  islidlm  14753  lidlacl  14758  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  rspsn  14808  psrval  14940  psradd  14960  mpladd  14985  blfvalps  15376  lgseisenlem3  16071  lgseisenlem4  16072