Theorem oveqd 6045

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 6034	. 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 6028

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  oveq123d  6049  oveqdr  6056  csbov12g  6068  ovmpodxf  6157  oprssov  6174  ofeqd  6246  ofeq  6247  fnmpoovd  6389  seqeq2  10776  prdsex  13432  prdsval  13436  pwsplusgval  13458  pwsmulrval  13459  imasex  13468  imasival  13469  plusffvalg  13525  mgm1  13533  grpidvalg  13536  grpidd  13546  gsumress  13558  sgrp1  13574  issgrpd  13575  ismndd  13600  issubmnd  13605  mnd1  13618  ismhm  13624  mhmex  13625  issubm  13635  resmhm  13650  resmhm2  13651  resmhm2b  13652  isgrp  13669  isgrpd2e  13683  grpidd2  13704  grpinvfvalg  13705  grp1  13769  imasgrp2  13777  imasgrp  13778  subg0  13847  subginv  13848  subgcl  13851  issubgrpd2  13857  isnsg  13869  nmznsg  13880  isghm  13910  resghm  13927  iscmn  13960  iscmnd  13965  imasabl  14003  rngass  14033  rngcl  14038  rngpropd  14049  dfur2g  14056  issrg  14059  srgcl  14064  srgass  14065  srgideu  14066  issrgid  14075  srgpcomp  14084  srgpcompp  14085  isring  14094  ringcl  14107  crngcom  14108  iscrng2  14109  ringass  14110  ringideu  14111  isringid  14119  ringidss  14123  ringpropd  14132  ring1  14153  opprmulg  14165  oppr0g  14175  oppr1g  14176  opprnegg  14177  mulgass3  14179  dvdsrvald  14188  dvdsrd  14189  opprunitd  14205  dvrvald  14229  rdivmuldivd  14239  rhmmul  14259  isrhm2d  14260  rhmopp  14271  rhmunitinv  14273  islring  14287  lringuplu  14291  subrngmcl  14304  subrg1  14326  subrgmcl  14328  subrgdvds  14330  subrguss  14331  subrginv  14332  subrgdv  14333  subrgunit  14334  subrgugrp  14335  issubrg3  14342  rhmpropd  14349  rrgval  14357  aprval  14378  aprap  14382  islmod  14387  islmodd  14389  scaffvalg  14402  lmodpropd  14445  lsssetm  14452  islssmd  14455  islidlm  14575  lidlacl  14580  rnglidlmmgm  14592  rnglidlmsgrp  14593  rnglidlrng  14594  rspsn  14630  psrval  14762  psradd  14780  mpladd  14805  blfvalps  15196  lgseisenlem3  15891  lgseisenlem4  15892