Theorem oveqd 6034

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 6023	. 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 1397  (class class class)co 6017

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  oveq123d  6038  oveqdr  6045  csbov12g  6057  ovmpodxf  6146  oprssov  6163  ofeqd  6236  ofeq  6237  fnmpoovd  6379  seqeq2  10712  prdsex  13351  prdsval  13355  pwsplusgval  13377  pwsmulrval  13378  imasex  13387  imasival  13388  plusffvalg  13444  mgm1  13452  grpidvalg  13455  grpidd  13465  gsumress  13477  sgrp1  13493  issgrpd  13494  ismndd  13519  issubmnd  13524  mnd1  13537  ismhm  13543  mhmex  13544  issubm  13554  resmhm  13569  resmhm2  13570  resmhm2b  13571  isgrp  13588  isgrpd2e  13602  grpidd2  13623  grpinvfvalg  13624  grp1  13688  imasgrp2  13696  imasgrp  13697  subg0  13766  subginv  13767  subgcl  13770  issubgrpd2  13776  isnsg  13788  nmznsg  13799  isghm  13829  resghm  13846  iscmn  13879  iscmnd  13884  imasabl  13922  rngass  13951  rngcl  13956  rngpropd  13967  dfur2g  13974  issrg  13977  srgcl  13982  srgass  13983  srgideu  13984  issrgid  13993  srgpcomp  14002  srgpcompp  14003  isring  14012  ringcl  14025  crngcom  14026  iscrng2  14027  ringass  14028  ringideu  14029  isringid  14037  ringidss  14041  ringpropd  14050  ring1  14071  opprmulg  14083  oppr0g  14093  oppr1g  14094  opprnegg  14095  mulgass3  14097  dvdsrvald  14106  dvdsrd  14107  opprunitd  14123  dvrvald  14147  rdivmuldivd  14157  rhmmul  14177  isrhm2d  14178  rhmopp  14189  rhmunitinv  14191  islring  14205  lringuplu  14209  subrngmcl  14222  subrg1  14244  subrgmcl  14246  subrgdvds  14248  subrguss  14249  subrginv  14250  subrgdv  14251  subrgunit  14252  subrgugrp  14253  issubrg3  14260  rhmpropd  14267  rrgval  14275  aprval  14295  aprap  14299  islmod  14304  islmodd  14306  scaffvalg  14319  lmodpropd  14362  lsssetm  14369  islssmd  14372  islidlm  14492  lidlacl  14497  rnglidlmmgm  14509  rnglidlmsgrp  14510  rnglidlrng  14511  rspsn  14547  psrval  14679  psradd  14692  mpladd  14717  blfvalps  15108  lgseisenlem3  15800  lgseisenlem4  15801