Theorem oveqd 6035

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 6024	. 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 6018

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 6021

This theorem is referenced by:  oveq123d  6039  oveqdr  6046  csbov12g  6058  ovmpodxf  6147  oprssov  6164  ofeqd  6237  ofeq  6238  fnmpoovd  6380  seqeq2  10714  prdsex  13370  prdsval  13374  pwsplusgval  13396  pwsmulrval  13397  imasex  13406  imasival  13407  plusffvalg  13463  mgm1  13471  grpidvalg  13474  grpidd  13484  gsumress  13496  sgrp1  13512  issgrpd  13513  ismndd  13538  issubmnd  13543  mnd1  13556  ismhm  13562  mhmex  13563  issubm  13573  resmhm  13588  resmhm2  13589  resmhm2b  13590  isgrp  13607  isgrpd2e  13621  grpidd2  13642  grpinvfvalg  13643  grp1  13707  imasgrp2  13715  imasgrp  13716  subg0  13785  subginv  13786  subgcl  13789  issubgrpd2  13795  isnsg  13807  nmznsg  13818  isghm  13848  resghm  13865  iscmn  13898  iscmnd  13903  imasabl  13941  rngass  13971  rngcl  13976  rngpropd  13987  dfur2g  13994  issrg  13997  srgcl  14002  srgass  14003  srgideu  14004  issrgid  14013  srgpcomp  14022  srgpcompp  14023  isring  14032  ringcl  14045  crngcom  14046  iscrng2  14047  ringass  14048  ringideu  14049  isringid  14057  ringidss  14061  ringpropd  14070  ring1  14091  opprmulg  14103  oppr0g  14113  oppr1g  14114  opprnegg  14115  mulgass3  14117  dvdsrvald  14126  dvdsrd  14127  opprunitd  14143  dvrvald  14167  rdivmuldivd  14177  rhmmul  14197  isrhm2d  14198  rhmopp  14209  rhmunitinv  14211  islring  14225  lringuplu  14229  subrngmcl  14242  subrg1  14264  subrgmcl  14266  subrgdvds  14268  subrguss  14269  subrginv  14270  subrgdv  14271  subrgunit  14272  subrgugrp  14273  issubrg3  14280  rhmpropd  14287  rrgval  14295  aprval  14315  aprap  14319  islmod  14324  islmodd  14326  scaffvalg  14339  lmodpropd  14382  lsssetm  14389  islssmd  14392  islidlm  14512  lidlacl  14517  rnglidlmmgm  14529  rnglidlmsgrp  14530  rnglidlrng  14531  rspsn  14567  psrval  14699  psradd  14712  mpladd  14737  blfvalps  15128  lgseisenlem3  15820  lgseisenlem4  15821