Theorem oveqd 6095

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 6084	. 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 1402  (class class class)co 6078

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081

This theorem is referenced by:  oveq123d  6099  oveqdr  6106  csbov12g  6118  ovmpodxf  6207  oprssov  6224  ofeqd  6297  ofeq  6298  fnmpoovd  6444  seqeq2  10869  imasex  13606  imasival  13607  plusffvalg  13662  mgm1  13670  grpidvalg  13673  grpidd  13683  gzsumress  13692  sgrp1  13706  issgrpd  13707  ismndd  13730  issubmnd  13735  mnd1  13742  ismhm  13748  mhmex  13749  issubm  13759  resmhm  13774  resmhm2  13775  resmhm2b  13776  isgrp  13791  isgrpd2e  13805  grpidd2  13826  grpinvfvalg  13827  grp1  13891  imasgrp2  13893  imasgrp  13894  subg0  13963  subginv  13964  subgcl  13967  issubgrpd2  13973  isnsg  13985  nmznsg  13996  isghm  14026  resghm  14043  iscmn  14076  iscmnd  14081  cmnsubm  14092  imasabl  14120  prdsex  14152  prdsval  14153  pwsplusgval  14188  pwsmulrval  14189  rngass  14216  rngcl  14221  rngpropd  14232  dfur2g  14243  issrg  14246  srgcl  14251  srgass  14252  srgideu  14253  issrgid  14262  srgpcomp  14271  srgpcompp  14272  isring  14281  ringcl  14294  crngcom  14295  iscrng2  14296  ringass  14297  ringideu  14298  isringid  14306  ringidss  14310  ringpropd  14319  ring1  14340  opprmulg  14352  oppr0g  14363  oppr1g  14364  opprnegg  14365  mulgass3  14367  dvdsrvald  14376  dvdsrd  14377  opprunitd  14393  dvrvald  14417  rdivmuldivd  14427  rhmmul  14447  isrhm2d  14448  rhmopp  14459  rhmunitinv  14461  islring  14475  lringuplu  14479  opprlring  14480  subrngmcl  14493  subrg1  14515  subrgmcl  14517  subrgdvds  14519  subrguss  14520  subrginv  14521  subrgdv  14522  subrgunit  14523  subrgugrp  14524  issubrg3  14531  rhmpropd  14538  rrgval  14546  aprval  14567  aprap  14574  aprprop  14577  islmod  14603  islmodd  14605  scaffvalg  14618  lmodpropd  14661  lsssetm  14668  islssmd  14671  islidlm  14791  lidlacl  14796  rnglidlmmgm  14808  rnglidlmsgrp  14809  rnglidlrng  14810  rspsn  14846  psrval  14976  psradd  14996  mpladd  15021  blfvalps  15412  lgseisenlem3  16108  lgseisenlem4  16109