Theorem oveqi 7382

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

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

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 3446  df-ss 3928  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  oveq123i  7383  fvmpopr2d  7531  cantnfval2  9600  vdwap1  16925  vdwlem12  16940  prdsdsval3  17425  oppchom  17657  rcaninv  17737  initoeu2lem0  17956  yonedalem21  18215  yonedalem22  18220  issubmgm  18612  mndprop  18670  issubm  18713  frmdadd  18765  smndex1sgrp  18818  smndex1mnd  18820  grpprop  18867  oppgplus  19264  ablprop  19708  ringpropd  20209  crngpropd  20210  ringprop  20211  opprmul  20261  opprrngb  20267  opprringb  20269  mulgass3  20274  rngidpropd  20336  invrpropd  20339  rhmimasubrng  20487  cntzsubrng  20488  subrngpropd  20489  subrgpropd  20529  rhmpropd  20530  rhmsubclem4  20609  drngprop  20665  lidlacl  21164  lidlrsppropd  21187  crngridl  21223  pzriprnglem5  21428  pzriprnglem6  21429  pzriprng1ALT  21439  psradd  21880  ressmpladd  21970  ressmplmul  21971  ressmplvsca  21972  ressply1add  22148  ressply1mul  22149  ressply1vsca  22150  ply1coe  22219  evls1addd  22292  evls1muld  22293  evls1vsca  22294  rhmply1  22307  rhmply1vsca  22309  scmatscmiddistr  22429  1marepvsma1  22504  decpmatmulsumfsupp  22694  pmatcollpw1lem2  22696  pmatcollpwscmatlem1  22710  mptcoe1matfsupp  22723  mp2pm2mplem4  22730  chmatval  22750  chpidmat  22768  xpsdsval  24303  blres  24353  nmfval0  24512  nmval2  24514  ngpocelbl  24626  cncfmet  24836  ehl2eudisval  25357  minveclem2  25360  minveclem3b  25362  minveclem4  25366  minveclem6  25368  ply1divalg2  26078  clwwlknon1  30077  clwwlknon1nloop  30079  clwwlknon2  30082  nvm  30621  opprqusplusg  33454  zringfrac  33519  evls1subd  33535  algextdeglem8  33708  madjusmdetlem1  33811  xrge0pluscn  33924  esumpfinvallem  34058  ptrecube  37608  equivbnd2  37780  ismtyres  37796  iccbnd  37828  exidreslem  37865  iscrngo2  37985  toycom  38960  aks6d1c1p5  42094  aks5lem3a  42171  frlmsnic  42522  mendplusgfval  43164  sge0tsms  46372  vonn0ioo  46679  vonn0icc  46680  zlmodzxzadd  48340  snlindsntor  48454  ovsng2  48841  isisod  49010  upeu2lem  49011  imaidfu  49093  cofuswapf2  49278  indthinc  49445  indthincALT  49446  prsthinc  49447  lmddu  49650