Theorem oveqd 6038

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

Syntax hints:   → wi 4   = wceq 1397  (class class class)co 6021

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 6024

This theorem is referenced by:  oveq123d  6042  oveqdr  6049  csbov12g  6061  ovmpodxf  6150  oprssov  6167  ofeqd  6240  ofeq  6241  fnmpoovd  6383  seqeq2  10717  prdsex  13373  prdsval  13377  pwsplusgval  13399  pwsmulrval  13400  imasex  13409  imasival  13410  plusffvalg  13466  mgm1  13474  grpidvalg  13477  grpidd  13487  gsumress  13499  sgrp1  13515  issgrpd  13516  ismndd  13541  issubmnd  13546  mnd1  13559  ismhm  13565  mhmex  13566  issubm  13576  resmhm  13591  resmhm2  13592  resmhm2b  13593  isgrp  13610  isgrpd2e  13624  grpidd2  13645  grpinvfvalg  13646  grp1  13710  imasgrp2  13718  imasgrp  13719  subg0  13788  subginv  13789  subgcl  13792  issubgrpd2  13798  isnsg  13810  nmznsg  13821  isghm  13851  resghm  13868  iscmn  13901  iscmnd  13906  imasabl  13944  rngass  13974  rngcl  13979  rngpropd  13990  dfur2g  13997  issrg  14000  srgcl  14005  srgass  14006  srgideu  14007  issrgid  14016  srgpcomp  14025  srgpcompp  14026  isring  14035  ringcl  14048  crngcom  14049  iscrng2  14050  ringass  14051  ringideu  14052  isringid  14060  ringidss  14064  ringpropd  14073  ring1  14094  opprmulg  14106  oppr0g  14116  oppr1g  14117  opprnegg  14118  mulgass3  14120  dvdsrvald  14129  dvdsrd  14130  opprunitd  14146  dvrvald  14170  rdivmuldivd  14180  rhmmul  14200  isrhm2d  14201  rhmopp  14212  rhmunitinv  14214  islring  14228  lringuplu  14232  subrngmcl  14245  subrg1  14267  subrgmcl  14269  subrgdvds  14271  subrguss  14272  subrginv  14273  subrgdv  14274  subrgunit  14275  subrgugrp  14276  issubrg3  14283  rhmpropd  14290  rrgval  14298  aprval  14318  aprap  14322  islmod  14327  islmodd  14329  scaffvalg  14342  lmodpropd  14385  lsssetm  14392  islssmd  14395  islidlm  14515  lidlacl  14520  rnglidlmmgm  14532  rnglidlmsgrp  14533  rnglidlrng  14534  rspsn  14570  psrval  14702  psradd  14720  mpladd  14745  blfvalps  15136  lgseisenlem3  15828  lgseisenlem4  15829