Theorem oveqi 7422

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  oveq123i  7423  fvmpopr2d  7569  cantnfval2  9664  vdwap1  16910  vdwlem12  16925  prdsdsval3  17431  oppchom  17660  rcaninv  17741  initoeu2lem0  17963  yonedalem21  18226  yonedalem22  18231  mndprop  18651  issubm  18684  frmdadd  18736  smndex1sgrp  18789  smndex1mnd  18791  grpprop  18838  oppgplus  19213  ablprop  19661  ringpropd  20102  crngpropd  20103  ringprop  20104  opprmul  20153  opprringb  20162  mulgass3  20167  rngidpropd  20229  invrpropd  20232  subrgpropd  20355  rhmpropd  20356  drngprop  20372  lidlacl  20836  lidlmcl  20840  lidlrsppropd  20855  crngridl  20876  psradd  21501  ressmpladd  21584  ressmplmul  21585  ressmplvsca  21586  ressply1add  21752  ressply1mul  21753  ressply1vsca  21754  ply1coe  21820  scmatscmiddistr  22010  1marepvsma1  22085  decpmatmulsumfsupp  22275  pmatcollpw1lem2  22277  pmatcollpwscmatlem1  22291  mptcoe1matfsupp  22304  mp2pm2mplem4  22311  chmatval  22331  chpidmat  22349  xpsdsval  23887  blres  23937  nmfval0  24099  nmval2  24101  ngpocelbl  24221  cncfmet  24425  ehl2eudisval  24940  minveclem2  24943  minveclem3b  24945  minveclem4  24949  minveclem6  24951  ply1divalg2  25656  clwwlknon1  29350  clwwlknon1nloop  29352  clwwlknon2  29355  nvm  29894  opprqusplusg  32603  evls1addd  32648  evls1muld  32649  evls1vsca  32650  madjusmdetlem1  32807  xrge0pluscn  32920  esumpfinvallem  33072  ptrecube  36488  equivbnd2  36660  ismtyres  36676  iccbnd  36708  exidreslem  36745  iscrngo2  36865  toycom  37843  frlmsnic  41110  mendplusgfval  41927  sge0tsms  45096  vonn0ioo  45403  vonn0icc  45404  issubmgm  46559  opprrngb  46675  rhmimasubrng  46745  cntzsubrng  46746  subrngpropd  46747  pzriprnglem5  46809  pzriprnglem6  46810  pzriprng1ALT  46820  rhmsubclem4  46987  zlmodzxzadd  47034  snlindsntor  47152  indthinc  47672  indthincALT  47673  prsthinc  47674  mndtchom  47710