Theorem oveqd 6075

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

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

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 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  oveq123d  6079  oveqdr  6086  csbov12g  6098  ovmpodxf  6187  oprssov  6204  ofeqd  6277  ofeq  6278  fnmpoovd  6424  seqeq2  10840  imasex  13572  imasival  13573  plusffvalg  13628  mgm1  13636  grpidvalg  13639  grpidd  13649  gsumress  13661  sgrp1  13677  issgrpd  13678  ismndd  13701  issubmnd  13706  mnd1  13713  ismhm  13719  mhmex  13720  issubm  13730  resmhm  13745  resmhm2  13746  resmhm2b  13747  isgrp  13764  isgrpd2e  13778  grpidd2  13799  grpinvfvalg  13800  grp1  13864  imasgrp2  13866  imasgrp  13867  subg0  13936  subginv  13937  subgcl  13940  issubgrpd2  13946  isnsg  13958  nmznsg  13969  isghm  13999  resghm  14016  iscmn  14049  iscmnd  14054  imasabl  14092  prdsex  14117  prdsval  14118  pwsplusgval  14153  pwsmulrval  14154  rngass  14181  rngcl  14186  rngpropd  14197  dfur2g  14208  issrg  14211  srgcl  14216  srgass  14217  srgideu  14218  issrgid  14227  srgpcomp  14236  srgpcompp  14237  isring  14246  ringcl  14259  crngcom  14260  iscrng2  14261  ringass  14262  ringideu  14263  isringid  14271  ringidss  14275  ringpropd  14284  ring1  14305  opprmulg  14317  oppr0g  14328  oppr1g  14329  opprnegg  14330  mulgass3  14332  dvdsrvald  14341  dvdsrd  14342  opprunitd  14358  dvrvald  14382  rdivmuldivd  14392  rhmmul  14412  isrhm2d  14413  rhmopp  14424  rhmunitinv  14426  islring  14440  lringuplu  14444  opprlring  14445  subrngmcl  14458  subrg1  14480  subrgmcl  14482  subrgdvds  14484  subrguss  14485  subrginv  14486  subrgdv  14487  subrgunit  14488  subrgugrp  14489  issubrg3  14496  rhmpropd  14503  rrgval  14511  aprval  14532  aprap  14539  aprprop  14542  islmod  14568  islmodd  14570  scaffvalg  14583  lmodpropd  14626  lsssetm  14633  islssmd  14636  islidlm  14756  lidlacl  14761  rnglidlmmgm  14773  rnglidlmsgrp  14774  rnglidlrng  14775  rspsn  14811  psrval  14943  psradd  14963  mpladd  14988  blfvalps  15379  lgseisenlem3  16074  lgseisenlem4  16075