Theorem oveqi 7362

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 7355	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)

Syntax hints:   = wceq 1540  (class class class)co 7349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  oveq123i  7363  fvmpopr2d  7511  cantnfval2  9565  vdwap1  16889  vdwlem12  16904  prdsdsval3  17389  oppchom  17621  rcaninv  17701  initoeu2lem0  17920  yonedalem21  18179  yonedalem22  18184  issubmgm  18576  mndprop  18634  issubm  18677  frmdadd  18729  smndex1sgrp  18782  smndex1mnd  18784  grpprop  18831  oppgplus  19228  ablprop  19672  ringpropd  20173  crngpropd  20174  ringprop  20175  opprmul  20225  opprrngb  20231  opprringb  20233  mulgass3  20238  rngidpropd  20300  invrpropd  20303  rhmimasubrng  20451  cntzsubrng  20452  subrngpropd  20453  subrgpropd  20493  rhmpropd  20494  rhmsubclem4  20573  drngprop  20629  lidlacl  21128  lidlrsppropd  21151  crngridl  21187  pzriprnglem5  21392  pzriprnglem6  21393  pzriprng1ALT  21403  psradd  21844  ressmpladd  21934  ressmplmul  21935  ressmplvsca  21936  ressply1add  22112  ressply1mul  22113  ressply1vsca  22114  ply1coe  22183  evls1addd  22256  evls1muld  22257  evls1vsca  22258  rhmply1  22271  rhmply1vsca  22273  scmatscmiddistr  22393  1marepvsma1  22468  decpmatmulsumfsupp  22658  pmatcollpw1lem2  22660  pmatcollpwscmatlem1  22674  mptcoe1matfsupp  22687  mp2pm2mplem4  22694  chmatval  22714  chpidmat  22732  xpsdsval  24267  blres  24317  nmfval0  24476  nmval2  24478  ngpocelbl  24590  cncfmet  24800  ehl2eudisval  25321  minveclem2  25324  minveclem3b  25326  minveclem4  25330  minveclem6  25332  ply1divalg2  26042  clwwlknon1  30045  clwwlknon1nloop  30047  clwwlknon2  30050  nvm  30589  opprqusplusg  33435  zringfrac  33500  evls1subd  33516  algextdeglem8  33707  madjusmdetlem1  33810  xrge0pluscn  33923  esumpfinvallem  34057  ptrecube  37620  equivbnd2  37792  ismtyres  37808  iccbnd  37840  exidreslem  37877  iscrngo2  37997  toycom  38972  aks6d1c1p5  42105  aks5lem3a  42182  frlmsnic  42533  mendplusgfval  43174  sge0tsms  46381  vonn0ioo  46688  vonn0icc  46689  zlmodzxzadd  48362  snlindsntor  48476  ovsng2  48863  isisod  49032  upeu2lem  49033  imaidfu  49115  cofuswapf2  49300  indthinc  49467  indthincALT  49468  prsthinc  49469  lmddu  49672