Theorem oveqi 7369

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-ss 3902  df-uni 4841  df-br 5075  df-iota 6443  df-fv 6495  df-ov 7359

This theorem is referenced by:  oveq123i  7370  fvmpopr2d  7518  cantnfval2  9579  vdwap1  16937  vdwlem12  16952  prdsdsval3  17437  oppchom  17670  rcaninv  17750  initoeu2lem0  17969  yonedalem21  18228  yonedalem22  18233  issubmgm  18659  mndprop  18717  issubm  18760  frmdadd  18812  smndex1sgrp  18868  smndex1mnd  18870  grpprop  18917  oppgplus  19313  ablprop  19757  ringpropd  20258  crngpropd  20259  ringprop  20260  opprmul  20309  opprrngb  20315  opprringb  20317  mulgass3  20322  rngidpropd  20384  invrpropd  20387  rhmimasubrng  20532  cntzsubrng  20533  subrngpropd  20534  subrgpropd  20574  rhmpropd  20575  rhmsubclem4  20654  drngprop  20710  lidlacl  21208  lidlrsppropd  21231  crngridl  21267  pzriprnglem5  21454  pzriprnglem6  21455  pzriprng1ALT  21465  psradd  21906  ressmpladd  21996  ressmplmul  21997  ressmplvsca  21998  ressply1add  22181  ressply1mul  22182  ressply1vsca  22183  ply1coe  22251  evls1addd  22324  evls1muld  22325  evls1vsca  22326  rhmply1  22339  rhmply1vsca  22341  scmatscmiddistr  22461  1marepvsma1  22536  decpmatmulsumfsupp  22726  pmatcollpw1lem2  22728  pmatcollpwscmatlem1  22742  mptcoe1matfsupp  22755  mp2pm2mplem4  22762  chmatval  22782  chpidmat  22800  xpsdsval  24334  blres  24384  nmfval0  24543  nmval2  24545  ngpocelbl  24657  cncfmet  24864  ehl2eudisval  25378  minveclem2  25381  minveclem3b  25383  minveclem4  25387  minveclem6  25389  ply1divalg2  26092  clwwlknon1  30155  clwwlknon1nloop  30157  clwwlknon2  30160  nvm  30700  opprqusplusg  33537  zringfrac  33602  evls1subd  33620  algextdeglem8  33856  madjusmdetlem1  33959  xrge0pluscn  34072  esumpfinvallem  34206  ptrecube  37929  equivbnd2  38101  ismtyres  38117  iccbnd  38149  exidreslem  38186  iscrngo2  38306  toycom  39407  aks6d1c1p5  42539  aks5lem3a  42616  frlmsnic  42973  mendplusgfval  43597  sge0tsms  46796  vonn0ioo  47103  vonn0icc  47104  zlmodzxzadd  48822  snlindsntor  48935  ovsng2  49322  isisod  49490  upeu2lem  49491  imaidfu  49573  cofuswapf2  49758  indthinc  49925  indthincALT  49926  prsthinc  49927  lmddu  50130