Theorem oveqd 6096

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 6085	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1402  (class class class)co 6079

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6082

This theorem is referenced by:  oveq123d  6100  oveqdr  6107  csbov12g  6119  ovmpodxf  6208  oprssov  6225  ofeqd  6298  ofeq  6299  fnmpoovd  6445  seqeq2  10871  imasex  13609  imasival  13610  plusffvalg  13665  mgm1  13673  grpidvalg  13676  grpidd  13686  gzsumress  13695  sgrp1  13709  issgrpd  13710  ismndd  13733  issubmnd  13738  mnd1  13745  ismhm  13751  mhmex  13752  issubm  13762  resmhm  13777  resmhm2  13778  resmhm2b  13779  isgrp  13794  isgrpd2e  13808  grpidd2  13829  grpinvfvalg  13830  grp1  13894  imasgrp2  13896  imasgrp  13897  subg0  13966  subginv  13967  subgcl  13970  issubgrpd2  13976  isnsg  13988  nmznsg  13999  isghm  14029  resghm  14046  iscmn  14079  iscmnd  14084  cmnsubm  14095  imasabl  14123  prdsex  14155  prdsval  14156  pwsplusgval  14191  pwsmulrval  14192  rngass  14221  rngcl  14226  rngpropd  14237  dfur2g  14249  issrg  14252  srgcl  14257  srgass  14258  srgideu  14259  issrgid  14268  srgpcomp  14277  srgpcompp  14278  isring  14287  ringcl  14300  crngcom  14301  iscrng2  14302  ringass  14303  ringideu  14304  isringid  14313  ringidss  14317  ringpropd  14326  ring1  14347  opprmulg  14359  oppr0g  14370  oppr1g  14371  opprnegg  14372  mulgass3  14374  dvdsrvald  14383  dvdsrd  14384  opprunitd  14400  dvrvald  14424  rdivmuldivd  14434  rhmmul  14454  isrhm2d  14455  rhmopp  14466  rhmunitinv  14468  islring  14482  lringuplu  14486  opprlring  14487  subrngmcl  14500  subrg1  14522  subrgmcl  14524  subrgdvds  14526  subrguss  14527  subrginv  14528  subrgdv  14529  subrgunit  14530  subrgugrp  14531  issubrg3  14538  rhmpropd  14545  rrgval  14553  aprval  14574  aprap  14581  aprprop  14584  islmod  14610  islmodd  14612  scaffvalg  14626  lmodpropd  14669  lsssetm  14676  islssmd  14679  islidlm  14799  lidlacl  14804  rnglidlmmgm  14816  rnglidlmsgrp  14817  rnglidlrng  14818  rspsn  14854  isassa  14985  isassad  14994  assamulgscmlem2  15025  psrval  15033  psradd  15053  mpladd  15078  blfvalps  15469  lgseisenlem3  16174  lgseisenlem4  16175