Theorem oveqd 6028

Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveqd	⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq 6017	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6011

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 3890  df-br 4085  df-iota 5282  df-fv 5330  df-ov 6014

This theorem is referenced by:  oveq123d  6032  oveqdr  6039  csbov12g  6051  ovmpodxf  6140  oprssov  6157  ofeqd  6230  ofeq  6231  fnmpoovd  6373  seqeq2  10701  prdsex  13339  prdsval  13343  pwsplusgval  13365  pwsmulrval  13366  imasex  13375  imasival  13376  plusffvalg  13432  mgm1  13440  grpidvalg  13443  grpidd  13453  gsumress  13465  sgrp1  13481  issgrpd  13482  ismndd  13507  issubmnd  13512  mnd1  13525  ismhm  13531  mhmex  13532  issubm  13542  resmhm  13557  resmhm2  13558  resmhm2b  13559  isgrp  13576  isgrpd2e  13590  grpidd2  13611  grpinvfvalg  13612  grp1  13676  imasgrp2  13684  imasgrp  13685  subg0  13754  subginv  13755  subgcl  13758  issubgrpd2  13764  isnsg  13776  nmznsg  13787  isghm  13817  resghm  13834  iscmn  13867  iscmnd  13872  imasabl  13910  rngass  13939  rngcl  13944  rngpropd  13955  dfur2g  13962  issrg  13965  srgcl  13970  srgass  13971  srgideu  13972  issrgid  13981  srgpcomp  13990  srgpcompp  13991  isring  14000  ringcl  14013  crngcom  14014  iscrng2  14015  ringass  14016  ringideu  14017  isringid  14025  ringidss  14029  ringpropd  14038  ring1  14059  opprmulg  14071  oppr0g  14081  oppr1g  14082  opprnegg  14083  mulgass3  14085  dvdsrvald  14094  dvdsrd  14095  opprunitd  14111  dvrvald  14135  rdivmuldivd  14145  rhmmul  14165  isrhm2d  14166  rhmopp  14177  rhmunitinv  14179  islring  14193  lringuplu  14197  subrngmcl  14210  subrg1  14232  subrgmcl  14234  subrgdvds  14236  subrguss  14237  subrginv  14238  subrgdv  14239  subrgunit  14240  subrgugrp  14241  issubrg3  14248  rhmpropd  14255  rrgval  14263  aprval  14283  aprap  14287  islmod  14292  islmodd  14294  scaffvalg  14307  lmodpropd  14350  lsssetm  14357  islssmd  14360  islidlm  14480  lidlacl  14485  rnglidlmmgm  14497  rnglidlmsgrp  14498  rnglidlrng  14499  rspsn  14535  psrval  14667  psradd  14680  mpladd  14705  blfvalps  15096  lgseisenlem3  15788  lgseisenlem4  15789