Theorem oveqd 5963

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 5952	. 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 1373  (class class class)co 5946

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  oveq123d  5967  oveqdr  5974  csbov12g  5986  ovmpodxf  6073  oprssov  6090  ofeqd  6162  ofeq  6163  fnmpoovd  6303  seqeq2  10598  prdsex  13134  prdsval  13138  pwsplusgval  13160  pwsmulrval  13161  imasex  13170  imasival  13171  plusffvalg  13227  mgm1  13235  grpidvalg  13238  grpidd  13248  gsumress  13260  sgrp1  13276  issgrpd  13277  ismndd  13302  issubmnd  13307  mnd1  13320  ismhm  13326  mhmex  13327  issubm  13337  resmhm  13352  resmhm2  13353  resmhm2b  13354  isgrp  13371  isgrpd2e  13385  grpidd2  13406  grpinvfvalg  13407  grp1  13471  imasgrp2  13479  imasgrp  13480  subg0  13549  subginv  13550  subgcl  13553  issubgrpd2  13559  isnsg  13571  nmznsg  13582  isghm  13612  resghm  13629  iscmn  13662  iscmnd  13667  imasabl  13705  rngass  13734  rngcl  13739  rngpropd  13750  dfur2g  13757  issrg  13760  srgcl  13765  srgass  13766  srgideu  13767  issrgid  13776  srgpcomp  13785  srgpcompp  13786  isring  13795  ringcl  13808  crngcom  13809  iscrng2  13810  ringass  13811  ringideu  13812  isringid  13820  ringidss  13824  ringpropd  13833  ring1  13854  opprmulg  13866  oppr0g  13876  oppr1g  13877  opprnegg  13878  mulgass3  13880  reldvdsrsrg  13887  dvdsrvald  13888  dvdsrd  13889  opprunitd  13905  dvrvald  13929  rdivmuldivd  13939  rhmmul  13959  isrhm2d  13960  rhmopp  13971  rhmunitinv  13973  islring  13987  lringuplu  13991  subrngmcl  14004  subrg1  14026  subrgmcl  14028  subrgdvds  14030  subrguss  14031  subrginv  14032  subrgdv  14033  subrgunit  14034  subrgugrp  14035  issubrg3  14042  rhmpropd  14049  rrgval  14057  aprval  14077  aprap  14081  islmod  14086  islmodd  14088  scaffvalg  14101  lmodpropd  14144  lsssetm  14151  islssmd  14154  islidlm  14274  lidlacl  14279  rnglidlmmgm  14291  rnglidlmsgrp  14292  rnglidlrng  14293  rspsn  14329  psrval  14461  psradd  14474  mpladd  14499  blfvalps  14890  lgseisenlem3  15582  lgseisenlem4  15583