Theorem oveqd 6077

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

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6060

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3921  df-br 4116  df-iota 5319  df-fv 5367  df-ov 6063

This theorem is referenced by:  oveq123d  6081  oveqdr  6088  csbov12g  6100  ovmpodxf  6189  oprssov  6206  ofeqd  6279  ofeq  6280  fnmpoovd  6426  seqeq2  10842  imasex  13575  imasival  13576  plusffvalg  13631  mgm1  13639  grpidvalg  13642  grpidd  13652  gzsumress  13661  sgrp1  13675  issgrpd  13676  ismndd  13699  issubmnd  13704  mnd1  13711  ismhm  13717  mhmex  13718  issubm  13728  resmhm  13743  resmhm2  13744  resmhm2b  13745  isgrp  13760  isgrpd2e  13774  grpidd2  13795  grpinvfvalg  13796  grp1  13860  imasgrp2  13862  imasgrp  13863  subg0  13932  subginv  13933  subgcl  13936  issubgrpd2  13942  isnsg  13954  nmznsg  13965  isghm  13995  resghm  14012  iscmn  14045  iscmnd  14050  cmnsubm  14061  imasabl  14089  prdsex  14121  prdsval  14122  pwsplusgval  14157  pwsmulrval  14158  rngass  14185  rngcl  14190  rngpropd  14201  dfur2g  14212  issrg  14215  srgcl  14220  srgass  14221  srgideu  14222  issrgid  14231  srgpcomp  14240  srgpcompp  14241  isring  14250  ringcl  14263  crngcom  14264  iscrng2  14265  ringass  14266  ringideu  14267  isringid  14275  ringidss  14279  ringpropd  14288  ring1  14309  opprmulg  14321  oppr0g  14332  oppr1g  14333  opprnegg  14334  mulgass3  14336  dvdsrvald  14345  dvdsrd  14346  opprunitd  14362  dvrvald  14386  rdivmuldivd  14396  rhmmul  14416  isrhm2d  14417  rhmopp  14428  rhmunitinv  14430  islring  14444  lringuplu  14448  opprlring  14449  subrngmcl  14462  subrg1  14484  subrgmcl  14486  subrgdvds  14488  subrguss  14489  subrginv  14490  subrgdv  14491  subrgunit  14492  subrgugrp  14493  issubrg3  14500  rhmpropd  14507  rrgval  14515  aprval  14536  aprap  14543  aprprop  14546  islmod  14572  islmodd  14574  scaffvalg  14587  lmodpropd  14630  lsssetm  14637  islssmd  14640  islidlm  14760  lidlacl  14765  rnglidlmmgm  14777  rnglidlmsgrp  14778  rnglidlrng  14779  rspsn  14815  psrval  14945  psradd  14965  mpladd  14990  blfvalps  15381  lgseisenlem3  16076  lgseisenlem4  16077