Theorem oveqd 6024

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 6013	. 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 1395  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  oveq123d  6028  oveqdr  6035  csbov12g  6047  ovmpodxf  6136  oprssov  6153  ofeqd  6226  ofeq  6227  fnmpoovd  6367  seqeq2  10685  prdsex  13318  prdsval  13322  pwsplusgval  13344  pwsmulrval  13345  imasex  13354  imasival  13355  plusffvalg  13411  mgm1  13419  grpidvalg  13422  grpidd  13432  gsumress  13444  sgrp1  13460  issgrpd  13461  ismndd  13486  issubmnd  13491  mnd1  13504  ismhm  13510  mhmex  13511  issubm  13521  resmhm  13536  resmhm2  13537  resmhm2b  13538  isgrp  13555  isgrpd2e  13569  grpidd2  13590  grpinvfvalg  13591  grp1  13655  imasgrp2  13663  imasgrp  13664  subg0  13733  subginv  13734  subgcl  13737  issubgrpd2  13743  isnsg  13755  nmznsg  13766  isghm  13796  resghm  13813  iscmn  13846  iscmnd  13851  imasabl  13889  rngass  13918  rngcl  13923  rngpropd  13934  dfur2g  13941  issrg  13944  srgcl  13949  srgass  13950  srgideu  13951  issrgid  13960  srgpcomp  13969  srgpcompp  13970  isring  13979  ringcl  13992  crngcom  13993  iscrng2  13994  ringass  13995  ringideu  13996  isringid  14004  ringidss  14008  ringpropd  14017  ring1  14038  opprmulg  14050  oppr0g  14060  oppr1g  14061  opprnegg  14062  mulgass3  14064  dvdsrvald  14073  dvdsrd  14074  opprunitd  14090  dvrvald  14114  rdivmuldivd  14124  rhmmul  14144  isrhm2d  14145  rhmopp  14156  rhmunitinv  14158  islring  14172  lringuplu  14176  subrngmcl  14189  subrg1  14211  subrgmcl  14213  subrgdvds  14215  subrguss  14216  subrginv  14217  subrgdv  14218  subrgunit  14219  subrgugrp  14220  issubrg3  14227  rhmpropd  14234  rrgval  14242  aprval  14262  aprap  14266  islmod  14271  islmodd  14273  scaffvalg  14286  lmodpropd  14329  lsssetm  14336  islssmd  14339  islidlm  14459  lidlacl  14464  rnglidlmmgm  14476  rnglidlmsgrp  14477  rnglidlrng  14478  rspsn  14514  psrval  14646  psradd  14659  mpladd  14684  blfvalps  15075  lgseisenlem3  15767  lgseisenlem4  15768