Theorem oveqd 5984

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 5973	. 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 1373  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  oveq123d  5988  oveqdr  5995  csbov12g  6007  ovmpodxf  6094  oprssov  6111  ofeqd  6183  ofeq  6184  fnmpoovd  6324  seqeq2  10633  prdsex  13216  prdsval  13220  pwsplusgval  13242  pwsmulrval  13243  imasex  13252  imasival  13253  plusffvalg  13309  mgm1  13317  grpidvalg  13320  grpidd  13330  gsumress  13342  sgrp1  13358  issgrpd  13359  ismndd  13384  issubmnd  13389  mnd1  13402  ismhm  13408  mhmex  13409  issubm  13419  resmhm  13434  resmhm2  13435  resmhm2b  13436  isgrp  13453  isgrpd2e  13467  grpidd2  13488  grpinvfvalg  13489  grp1  13553  imasgrp2  13561  imasgrp  13562  subg0  13631  subginv  13632  subgcl  13635  issubgrpd2  13641  isnsg  13653  nmznsg  13664  isghm  13694  resghm  13711  iscmn  13744  iscmnd  13749  imasabl  13787  rngass  13816  rngcl  13821  rngpropd  13832  dfur2g  13839  issrg  13842  srgcl  13847  srgass  13848  srgideu  13849  issrgid  13858  srgpcomp  13867  srgpcompp  13868  isring  13877  ringcl  13890  crngcom  13891  iscrng2  13892  ringass  13893  ringideu  13894  isringid  13902  ringidss  13906  ringpropd  13915  ring1  13936  opprmulg  13948  oppr0g  13958  oppr1g  13959  opprnegg  13960  mulgass3  13962  reldvdsrsrg  13969  dvdsrvald  13970  dvdsrd  13971  opprunitd  13987  dvrvald  14011  rdivmuldivd  14021  rhmmul  14041  isrhm2d  14042  rhmopp  14053  rhmunitinv  14055  islring  14069  lringuplu  14073  subrngmcl  14086  subrg1  14108  subrgmcl  14110  subrgdvds  14112  subrguss  14113  subrginv  14114  subrgdv  14115  subrgunit  14116  subrgugrp  14117  issubrg3  14124  rhmpropd  14131  rrgval  14139  aprval  14159  aprap  14163  islmod  14168  islmodd  14170  scaffvalg  14183  lmodpropd  14226  lsssetm  14233  islssmd  14236  islidlm  14356  lidlacl  14361  rnglidlmmgm  14373  rnglidlmsgrp  14374  rnglidlrng  14375  rspsn  14411  psrval  14543  psradd  14556  mpladd  14581  blfvalps  14972  lgseisenlem3  15664  lgseisenlem4  15665