Theorem oveqi 7268

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

Syntax hints:   = wceq 1539  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  oveq123i  7269  fvmpopr2d  7412  cantnfval2  9357  vdwap1  16606  vdwlem12  16621  prdsdsval3  17113  oppchom  17342  rcaninv  17423  initoeu2lem0  17644  yonedalem21  17907  yonedalem22  17912  mndprop  18326  issubm  18357  frmdadd  18409  smndex1sgrp  18462  smndex1mnd  18464  grpprop  18510  oppgplus  18868  ablprop  19313  ringpropd  19736  crngpropd  19737  ringprop  19738  opprmul  19780  opprringb  19789  mulgass3  19794  rngidpropd  19852  invrpropd  19855  drngprop  19917  subrgpropd  19974  rhmpropd  19975  lidlacl  20397  lidlmcl  20401  lidlrsppropd  20414  crngridl  20422  psradd  21061  ressmpladd  21140  ressmplmul  21141  ressmplvsca  21142  ressply1add  21311  ressply1mul  21312  ressply1vsca  21313  ply1coe  21377  scmatscmiddistr  21565  1marepvsma1  21640  decpmatmulsumfsupp  21830  pmatcollpw1lem2  21832  pmatcollpwscmatlem1  21846  mptcoe1matfsupp  21859  mp2pm2mplem4  21866  chmatval  21886  chpidmat  21904  xpsdsval  23442  blres  23492  nmfval0  23652  nmval2  23654  ngpocelbl  23774  cncfmet  23978  ehl2eudisval  24492  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem6  24503  ply1divalg2  25208  clwwlknon1  28362  clwwlknon1nloop  28364  clwwlknon2  28367  nvm  28904  madjusmdetlem1  31679  xrge0pluscn  31792  esumpfinvallem  31942  ptrecube  35704  equivbnd2  35877  ismtyres  35893  iccbnd  35925  exidreslem  35962  iscrngo2  36082  toycom  36914  frlmsnic  40188  mendplusgfval  40926  sge0tsms  43808  vonn0ioo  44115  vonn0icc  44116  issubmgm  45231  rhmsubclem4  45535  zlmodzxzadd  45582  snlindsntor  45700  indthinc  46221  indthincALT  46222  prsthinc  46223  mndtchom  46257