Theorem oveqi 7359

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

Syntax hints:   = wceq 1541  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  oveq123i  7360  fvmpopr2d  7508  cantnfval2  9559  vdwap1  16889  vdwlem12  16904  prdsdsval3  17389  oppchom  17621  rcaninv  17701  initoeu2lem0  17920  yonedalem21  18179  yonedalem22  18184  issubmgm  18610  mndprop  18668  issubm  18711  frmdadd  18763  smndex1sgrp  18816  smndex1mnd  18818  grpprop  18865  oppgplus  19261  ablprop  19705  ringpropd  20206  crngpropd  20207  ringprop  20208  opprmul  20258  opprrngb  20264  opprringb  20266  mulgass3  20271  rngidpropd  20333  invrpropd  20336  rhmimasubrng  20481  cntzsubrng  20482  subrngpropd  20483  subrgpropd  20523  rhmpropd  20524  rhmsubclem4  20603  drngprop  20659  lidlacl  21158  lidlrsppropd  21181  crngridl  21217  pzriprnglem5  21422  pzriprnglem6  21423  pzriprng1ALT  21433  psradd  21874  ressmpladd  21964  ressmplmul  21965  ressmplvsca  21966  ressply1add  22142  ressply1mul  22143  ressply1vsca  22144  ply1coe  22213  evls1addd  22286  evls1muld  22287  evls1vsca  22288  rhmply1  22301  rhmply1vsca  22303  scmatscmiddistr  22423  1marepvsma1  22498  decpmatmulsumfsupp  22688  pmatcollpw1lem2  22690  pmatcollpwscmatlem1  22704  mptcoe1matfsupp  22717  mp2pm2mplem4  22724  chmatval  22744  chpidmat  22762  xpsdsval  24296  blres  24346  nmfval0  24505  nmval2  24507  ngpocelbl  24619  cncfmet  24829  ehl2eudisval  25350  minveclem2  25353  minveclem3b  25355  minveclem4  25359  minveclem6  25361  ply1divalg2  26071  clwwlknon1  30077  clwwlknon1nloop  30079  clwwlknon2  30082  nvm  30621  opprqusplusg  33454  zringfrac  33519  evls1subd  33535  algextdeglem8  33737  madjusmdetlem1  33840  xrge0pluscn  33953  esumpfinvallem  34087  ptrecube  37659  equivbnd2  37831  ismtyres  37847  iccbnd  37879  exidreslem  37916  iscrngo2  38036  toycom  39071  aks6d1c1p5  42204  aks5lem3a  42281  frlmsnic  42632  mendplusgfval  43273  sge0tsms  46477  vonn0ioo  46784  vonn0icc  46785  zlmodzxzadd  48457  snlindsntor  48571  ovsng2  48958  isisod  49127  upeu2lem  49128  imaidfu  49210  cofuswapf2  49395  indthinc  49562  indthincALT  49563  prsthinc  49564  lmddu  49767