Theorem oveqi 7411

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

Syntax hints:   = wceq 1562  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  oveq123i  7412  fvmpopr2d  7560  cantnfval2  9626  vdwap1  17015  vdwlem12  17030  prdsdsval3  17516  oppchom  17749  rcaninv  17829  initoeu2lem0  18048  yonedalem21  18307  yonedalem22  18312  issubmgm  18738  mndprop  18796  issubm  18839  frmdadd  18891  smndex1sgrp  18947  smndex1mnd  18949  grpprop  18996  oppgplus  19391  ablprop  19835  ringpropd  20340  crngpropd  20341  ringprop  20342  opprmul  20391  opprrngb  20397  opprringb  20399  mulgass3  20404  rngidpropd  20466  invrpropd  20469  rhmimasubrng  20618  cntzsubrng  20619  subrngpropd  20620  subrgpropd  20660  rhmpropd  20661  rhmsubclem4  20740  drngprop  20796  lidlacl  21293  lidlrsppropd  21316  crngridl  21352  pzriprnglem5  21539  pzriprnglem6  21540  pzriprng1ALT  21550  psradd  21992  ressmpladd  22083  ressmplmul  22084  ressmplvsca  22085  ressply1add  22293  ressply1mul  22294  ressply1vsca  22295  ply1coe  22363  evls1addd  22436  evls1muld  22437  evls1vsca  22438  rhmply1  22448  rhmply1vsca  22450  scmatscmiddistr  22570  1marepvsma1  22645  decpmatmulsumfsupp  22835  pmatcollpw1lem2  22837  pmatcollpwscmatlem1  22851  mptcoe1matfsupp  22864  mp2pm2mplem4  22871  chmatval  22891  chpidmat  22909  xpsdsval  24443  blres  24493  nmfval0  24652  nmval2  24654  ngpocelbl  24766  cncfmet  24973  ehl2eudisval  25487  minveclem2  25490  minveclem3b  25492  minveclem4  25496  minveclem6  25498  ply1divalg2  26201  clwwlknon1  30301  clwwlknon1nloop  30303  clwwlknon2  30306  nvm  30846  opprqusplusg  33679  zringfrac  33752  evls1subd  33770  algextdeglem8  34023  madjusmdetlem1  34126  xrge0pluscn  34239  esumpfinvallem  34373  ptrecube  38124  equivbnd2  38296  ismtyres  38312  iccbnd  38344  exidreslem  38381  iscrngo2  38501  toycom  39602  aks6d1c1p5  42734  aks5lem3a  42811  frlmsnic  43163  mendplusgfval  43763  sge0tsms  46959  vonn0ioo  47266  vonn0icc  47267  zlmodzxzadd  48985  snlindsntor  49098  ovsng2  49485  isisod  49653  upeu2lem  49654  imaidfu  49736  cofuswapf2  49921  indthinc  50088  indthincALT  50089  prsthinc  50090  lmddu  50293