Theorem oveqi 7383

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

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

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 3444  df-ss 3920  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  oveq123i  7384  fvmpopr2d  7532  cantnfval2  9592  vdwap1  16919  vdwlem12  16934  prdsdsval3  17419  oppchom  17652  rcaninv  17732  initoeu2lem0  17951  yonedalem21  18210  yonedalem22  18215  issubmgm  18641  mndprop  18699  issubm  18742  frmdadd  18794  smndex1sgrp  18850  smndex1mnd  18852  grpprop  18899  oppgplus  19295  ablprop  19739  ringpropd  20240  crngpropd  20241  ringprop  20242  opprmul  20293  opprrngb  20299  opprringb  20301  mulgass3  20306  rngidpropd  20368  invrpropd  20371  rhmimasubrng  20516  cntzsubrng  20517  subrngpropd  20518  subrgpropd  20558  rhmpropd  20559  rhmsubclem4  20638  drngprop  20694  lidlacl  21193  lidlrsppropd  21216  crngridl  21252  pzriprnglem5  21457  pzriprnglem6  21458  pzriprng1ALT  21468  psradd  21910  ressmpladd  22001  ressmplmul  22002  ressmplvsca  22003  ressply1add  22187  ressply1mul  22188  ressply1vsca  22189  ply1coe  22259  evls1addd  22332  evls1muld  22333  evls1vsca  22334  rhmply1  22347  rhmply1vsca  22349  scmatscmiddistr  22469  1marepvsma1  22544  decpmatmulsumfsupp  22734  pmatcollpw1lem2  22736  pmatcollpwscmatlem1  22750  mptcoe1matfsupp  22763  mp2pm2mplem4  22770  chmatval  22790  chpidmat  22808  xpsdsval  24342  blres  24392  nmfval0  24551  nmval2  24553  ngpocelbl  24665  cncfmet  24875  ehl2eudisval  25396  minveclem2  25399  minveclem3b  25401  minveclem4  25405  minveclem6  25407  ply1divalg2  26117  clwwlknon1  30190  clwwlknon1nloop  30192  clwwlknon2  30195  nvm  30735  opprqusplusg  33588  zringfrac  33653  evls1subd  33671  algextdeglem8  33908  madjusmdetlem1  34011  xrge0pluscn  34124  esumpfinvallem  34258  ptrecube  37900  equivbnd2  38072  ismtyres  38088  iccbnd  38120  exidreslem  38157  iscrngo2  38277  toycom  39378  aks6d1c1p5  42511  aks5lem3a  42588  frlmsnic  42939  mendplusgfval  43567  sge0tsms  46767  vonn0ioo  47074  vonn0icc  47075  zlmodzxzadd  48747  snlindsntor  48860  ovsng2  49247  isisod  49415  upeu2lem  49416  imaidfu  49498  cofuswapf2  49683  indthinc  49850  indthincALT  49851  prsthinc  49852  lmddu  50055