Theorem oveqd 6035

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

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  13354  prdsval  13358  pwsplusgval  13380  pwsmulrval  13381  imasex  13390  imasival  13391  plusffvalg  13447  mgm1  13455  grpidvalg  13458  grpidd  13468  gsumress  13480  sgrp1  13496  issgrpd  13497  ismndd  13522  issubmnd  13527  mnd1  13540  ismhm  13546  mhmex  13547  issubm  13557  resmhm  13572  resmhm2  13573  resmhm2b  13574  isgrp  13591  isgrpd2e  13605  grpidd2  13626  grpinvfvalg  13627  grp1  13691  imasgrp2  13699  imasgrp  13700  subg0  13769  subginv  13770  subgcl  13773  issubgrpd2  13779  isnsg  13791  nmznsg  13802  isghm  13832  resghm  13849  iscmn  13882  iscmnd  13887  imasabl  13925  rngass  13955  rngcl  13960  rngpropd  13971  dfur2g  13978  issrg  13981  srgcl  13986  srgass  13987  srgideu  13988  issrgid  13997  srgpcomp  14006  srgpcompp  14007  isring  14016  ringcl  14029  crngcom  14030  iscrng2  14031  ringass  14032  ringideu  14033  isringid  14041  ringidss  14045  ringpropd  14054  ring1  14075  opprmulg  14087  oppr0g  14097  oppr1g  14098  opprnegg  14099  mulgass3  14101  dvdsrvald  14110  dvdsrd  14111  opprunitd  14127  dvrvald  14151  rdivmuldivd  14161  rhmmul  14181  isrhm2d  14182  rhmopp  14193  rhmunitinv  14195  islring  14209  lringuplu  14213  subrngmcl  14226  subrg1  14248  subrgmcl  14250  subrgdvds  14252  subrguss  14253  subrginv  14254  subrgdv  14255  subrgunit  14256  subrgugrp  14257  issubrg3  14264  rhmpropd  14271  rrgval  14279  aprval  14299  aprap  14303  islmod  14308  islmodd  14310  scaffvalg  14323  lmodpropd  14366  lsssetm  14373  islssmd  14376  islidlm  14496  lidlacl  14501  rnglidlmmgm  14513  rnglidlmsgrp  14514  rnglidlrng  14515  rspsn  14551  psrval  14683  psradd  14696  mpladd  14721  blfvalps  15112  lgseisenlem3  15804  lgseisenlem4  15805