Theorem oveqi 7377

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

Syntax hints:   = wceq 1542  (class class class)co 7364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-br 5087  df-iota 6452  df-fv 6504  df-ov 7367

This theorem is referenced by:  oveq123i  7378  fvmpopr2d  7526  cantnfval2  9587  vdwap1  16945  vdwlem12  16960  prdsdsval3  17445  oppchom  17678  rcaninv  17758  initoeu2lem0  17977  yonedalem21  18236  yonedalem22  18241  issubmgm  18667  mndprop  18725  issubm  18768  frmdadd  18820  smndex1sgrp  18876  smndex1mnd  18878  grpprop  18925  oppgplus  19321  ablprop  19765  ringpropd  20266  crngpropd  20267  ringprop  20268  opprmul  20317  opprrngb  20323  opprringb  20325  mulgass3  20330  rngidpropd  20392  invrpropd  20395  rhmimasubrng  20540  cntzsubrng  20541  subrngpropd  20542  subrgpropd  20582  rhmpropd  20583  rhmsubclem4  20662  drngprop  20718  lidlacl  21217  lidlrsppropd  21240  crngridl  21276  pzriprnglem5  21481  pzriprnglem6  21482  pzriprng1ALT  21492  psradd  21933  ressmpladd  22023  ressmplmul  22024  ressmplvsca  22025  ressply1add  22209  ressply1mul  22210  ressply1vsca  22211  ply1coe  22279  evls1addd  22352  evls1muld  22353  evls1vsca  22354  rhmply1  22367  rhmply1vsca  22369  scmatscmiddistr  22489  1marepvsma1  22564  decpmatmulsumfsupp  22754  pmatcollpw1lem2  22756  pmatcollpwscmatlem1  22770  mptcoe1matfsupp  22783  mp2pm2mplem4  22790  chmatval  22810  chpidmat  22828  xpsdsval  24362  blres  24412  nmfval0  24571  nmval2  24573  ngpocelbl  24685  cncfmet  24892  ehl2eudisval  25406  minveclem2  25409  minveclem3b  25411  minveclem4  25415  minveclem6  25417  ply1divalg2  26120  clwwlknon1  30188  clwwlknon1nloop  30190  clwwlknon2  30193  nvm  30733  opprqusplusg  33570  zringfrac  33635  evls1subd  33653  algextdeglem8  33890  madjusmdetlem1  33993  xrge0pluscn  34106  esumpfinvallem  34240  ptrecube  37963  equivbnd2  38135  ismtyres  38151  iccbnd  38183  exidreslem  38220  iscrngo2  38340  toycom  39441  aks6d1c1p5  42573  aks5lem3a  42650  frlmsnic  43007  mendplusgfval  43635  sge0tsms  46834  vonn0ioo  47141  vonn0icc  47142  zlmodzxzadd  48854  snlindsntor  48967  ovsng2  49354  isisod  49522  upeu2lem  49523  imaidfu  49605  cofuswapf2  49790  indthinc  49957  indthincALT  49958  prsthinc  49959  lmddu  50162