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  9598  vdwap1  16924  vdwlem12  16939  prdsdsval3  17424  oppchom  17656  rcaninv  17736  initoeu2lem0  17955  yonedalem21  18214  yonedalem22  18219  issubmgm  18611  mndprop  18669  issubm  18712  frmdadd  18764  smndex1sgrp  18817  smndex1mnd  18819  grpprop  18866  oppgplus  19263  ablprop  19707  ringpropd  20208  crngpropd  20209  ringprop  20210  opprmul  20260  opprrngb  20266  opprringb  20268  mulgass3  20273  rngidpropd  20335  invrpropd  20338  rhmimasubrng  20486  cntzsubrng  20487  subrngpropd  20488  subrgpropd  20528  rhmpropd  20529  rhmsubclem4  20608  drngprop  20664  lidlacl  21163  lidlrsppropd  21186  crngridl  21222  pzriprnglem5  21427  pzriprnglem6  21428  pzriprng1ALT  21438  psradd  21879  ressmpladd  21969  ressmplmul  21970  ressmplvsca  21971  ressply1add  22147  ressply1mul  22148  ressply1vsca  22149  ply1coe  22218  evls1addd  22291  evls1muld  22292  evls1vsca  22293  rhmply1  22306  rhmply1vsca  22308  scmatscmiddistr  22428  1marepvsma1  22503  decpmatmulsumfsupp  22693  pmatcollpw1lem2  22695  pmatcollpwscmatlem1  22709  mptcoe1matfsupp  22722  mp2pm2mplem4  22729  chmatval  22749  chpidmat  22767  xpsdsval  24302  blres  24352  nmfval0  24511  nmval2  24513  ngpocelbl  24625  cncfmet  24835  ehl2eudisval  25356  minveclem2  25359  minveclem3b  25361  minveclem4  25365  minveclem6  25367  ply1divalg2  26077  clwwlknon1  30076  clwwlknon1nloop  30078  clwwlknon2  30081  nvm  30620  opprqusplusg  33453  zringfrac  33518  evls1subd  33534  algextdeglem8  33707  madjusmdetlem1  33810  xrge0pluscn  33923  esumpfinvallem  34057  ptrecube  37607  equivbnd2  37779  ismtyres  37795  iccbnd  37827  exidreslem  37864  iscrngo2  37984  toycom  38959  aks6d1c1p5  42093  aks5lem3a  42170  frlmsnic  42521  mendplusgfval  43163  sge0tsms  46371  vonn0ioo  46678  vonn0icc  46679  zlmodzxzadd  48339  snlindsntor  48453  ovsng2  48840  isisod  49009  upeu2lem  49010  imaidfu  49092  cofuswapf2  49277  indthinc  49444  indthincALT  49445  prsthinc  49446  lmddu  49649