Theorem oveqd 6018

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 6007	. 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 6001

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 6004

This theorem is referenced by:  oveq123d  6022  oveqdr  6029  csbov12g  6041  ovmpodxf  6130  oprssov  6147  ofeqd  6220  ofeq  6221  fnmpoovd  6361  seqeq2  10673  prdsex  13302  prdsval  13306  pwsplusgval  13328  pwsmulrval  13329  imasex  13338  imasival  13339  plusffvalg  13395  mgm1  13403  grpidvalg  13406  grpidd  13416  gsumress  13428  sgrp1  13444  issgrpd  13445  ismndd  13470  issubmnd  13475  mnd1  13488  ismhm  13494  mhmex  13495  issubm  13505  resmhm  13520  resmhm2  13521  resmhm2b  13522  isgrp  13539  isgrpd2e  13553  grpidd2  13574  grpinvfvalg  13575  grp1  13639  imasgrp2  13647  imasgrp  13648  subg0  13717  subginv  13718  subgcl  13721  issubgrpd2  13727  isnsg  13739  nmznsg  13750  isghm  13780  resghm  13797  iscmn  13830  iscmnd  13835  imasabl  13873  rngass  13902  rngcl  13907  rngpropd  13918  dfur2g  13925  issrg  13928  srgcl  13933  srgass  13934  srgideu  13935  issrgid  13944  srgpcomp  13953  srgpcompp  13954  isring  13963  ringcl  13976  crngcom  13977  iscrng2  13978  ringass  13979  ringideu  13980  isringid  13988  ringidss  13992  ringpropd  14001  ring1  14022  opprmulg  14034  oppr0g  14044  oppr1g  14045  opprnegg  14046  mulgass3  14048  dvdsrvald  14057  dvdsrd  14058  opprunitd  14074  dvrvald  14098  rdivmuldivd  14108  rhmmul  14128  isrhm2d  14129  rhmopp  14140  rhmunitinv  14142  islring  14156  lringuplu  14160  subrngmcl  14173  subrg1  14195  subrgmcl  14197  subrgdvds  14199  subrguss  14200  subrginv  14201  subrgdv  14202  subrgunit  14203  subrgugrp  14204  issubrg3  14211  rhmpropd  14218  rrgval  14226  aprval  14246  aprap  14250  islmod  14255  islmodd  14257  scaffvalg  14270  lmodpropd  14313  lsssetm  14320  islssmd  14323  islidlm  14443  lidlacl  14448  rnglidlmmgm  14460  rnglidlmsgrp  14461  rnglidlrng  14462  rspsn  14498  psrval  14630  psradd  14643  mpladd  14668  blfvalps  15059  lgseisenlem3  15751  lgseisenlem4  15752