Theorem oveqi 7148

Description: Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveqi	⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)

Proof of Theorem oveqi

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq 7141	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)

Syntax hints:   = wceq 1538  (class class class)co 7135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  oveq123i  7149  fvmpopr2d  7290  cantnfval2  9116  vdwap1  16303  vdwlem12  16318  prdsdsval3  16750  oppchom  16977  rcaninv  17056  initoeu2lem0  17265  yonedalem21  17515  yonedalem22  17520  mndprop  17929  issubm  17960  frmdadd  18012  smndex1sgrp  18065  smndex1mnd  18067  grpprop  18111  oppgplus  18469  ablprop  18910  ringpropd  19328  crngpropd  19329  ringprop  19330  opprmul  19372  opprringb  19378  mulgass3  19383  rngidpropd  19441  invrpropd  19444  drngprop  19506  subrgpropd  19563  rhmpropd  19564  lidlacl  19979  lidlmcl  19983  lidlrsppropd  19996  crngridl  20004  psradd  20620  ressmpladd  20697  ressmplmul  20698  ressmplvsca  20699  ressply1add  20859  ressply1mul  20860  ressply1vsca  20861  ply1coe  20925  scmatscmiddistr  21113  1marepvsma1  21188  decpmatmulsumfsupp  21378  pmatcollpw1lem2  21380  pmatcollpwscmatlem1  21394  mptcoe1matfsupp  21407  mp2pm2mplem4  21414  chmatval  21434  chpidmat  21452  xpsdsval  22988  blres  23038  nmfval2  23197  nmval2  23198  ngpocelbl  23310  cncfmet  23514  ehl2eudisval  24027  minveclem2  24030  minveclem3b  24032  minveclem4  24036  minveclem6  24038  ply1divalg2  24739  clwwlknon1  27882  clwwlknon1nloop  27884  clwwlknon2  27887  nvm  28424  madjusmdetlem1  31180  xrge0pluscn  31293  esumpfinvallem  31443  ptrecube  35057  equivbnd2  35230  ismtyres  35246  iccbnd  35278  exidreslem  35315  iscrngo2  35435  toycom  36269  frlmsnic  39453  mendplusgfval  40129  sge0tsms  43019  vonn0ioo  43326  vonn0icc  43327  issubmgm  44409  rhmsubclem4  44713  zlmodzxzadd  44760  snlindsntor  44880