Theorem oveqi 7423

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

Syntax hints:   = wceq 1568  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  oveq123i  7424  fvmpopr2d  7572  cantnfval2  9637  vdwap1  17036  vdwlem12  17051  prdsdsval3  17537  oppchom  17770  rcaninv  17850  initoeu2lem0  18069  yonedalem21  18328  yonedalem22  18333  issubmgm  18759  mndprop  18817  issubm  18860  frmdadd  18913  smndex1sgrp  18969  smndex1mnd  18971  grpprop  19018  oppgplus  19418  ablprop  19862  ringpropd  20370  crngpropd  20371  ringprop  20372  opprmul  20421  opprrngb  20427  opprringb  20429  mulgass3  20434  rngidpropd  20496  invrpropd  20499  rhmimasubrng  20650  cntzsubrng  20651  subrngpropd  20652  subrgpropd  20692  rhmpropd  20693  rhmsubclem4  20772  drngprop  20829  lidlacl  21325  lidlrsppropd  21357  crngridl  21398  pzriprnglem5  21614  pzriprnglem6  21615  pzriprng1ALT  21625  psradd  22067  ressmpladd  22158  ressmplmul  22159  ressmplvsca  22160  ressply1add  22368  ressply1mul  22369  ressply1vsca  22370  ply1coe  22437  evls1addd  22510  evls1muld  22511  evls1vsca  22512  rhmply1  22522  rhmply1vsca  22524  scmatscmiddistr  22644  1marepvsma1  22719  decpmatmulsumfsupp  22909  pmatcollpw1lem2  22911  pmatcollpwscmatlem1  22925  mptcoe1matfsupp  22938  mp2pm2mplem4  22945  chmatval  22965  chpidmat  22983  xpsdsval  24517  blres  24567  nmfval0  24726  nmval2  24728  ngpocelbl  24840  cncfmet  25047  ehl2eudisval  25561  minveclem2  25564  minveclem3b  25566  minveclem4  25570  minveclem6  25572  ply1divalg2  26275  prlngmid2  29183  clwwlknon1  30414  clwwlknon1nloop  30416  clwwlknon2  30419  nvm  30959  opprqusplusg  33737  zringfrac  33810  evls1subd  33828  algextdeglem8  34080  madjusmdetlem1  34183  xrge0pluscn  34296  esumpfinvallem  34430  ptrecube  38215  equivbnd2  38387  ismtyres  38403  iccbnd  38435  exidreslem  38472  iscrngo2  38592  toycom  39693  aks6d1c1p5  42825  aks5lem3a  42902  frlmsnic  43256  mendplusgfval  43856  sge0tsms  47042  vonn0ioo  47349  vonn0icc  47350  zlmodzxzadd  49083  snlindsntor  49196  ovsng2  49582  isisod  49750  upeu2lem  49751  imaidfu  49833  cofuswapf2  50018  indthinc  50185  indthincALT  50186  prsthinc  50187  lmddu  50390