Theorem oveqi 6562

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

Syntax hints:   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  oveq123i  6563  cantnfval2  8449  vdwap1  15519  vdwlem12  15534  prdsdsval3  15968  oppchom  16198  rcaninv  16277  initoeu2lem0  16486  yonedalem21  16736  yonedalem22  16741  mndprop  17140  issubm  17170  frmdadd  17215  grpprop  17261  oppgplus  17602  ablprop  18027  ringpropd  18405  crngpropd  18406  ringprop  18407  opprmul  18449  opprringb  18455  mulgass3  18460  rngidpropd  18518  invrpropd  18521  drngprop  18581  subrgpropd  18637  rhmpropd  18638  lidlacl  19034  lidlmcl  19038  lidlrsppropd  19051  crngridl  19059  psradd  19203  ressmpladd  19278  ressmplmul  19279  ressmplvsca  19280  ressply1add  19421  ressply1mul  19422  ressply1vsca  19423  ply1coe  19487  scmatscmiddistr  20133  1marepvsma1  20208  decpmatmulsumfsupp  20397  pmatcollpw1lem2  20399  pmatcollpwscmatlem1  20413  mptcoe1matfsupp  20426  mp2pm2mplem4  20433  chmatval  20453  chpidmat  20471  xpsdsval  21996  blres  22046  nmfval2  22205  nmval2  22206  ngpocelbl  22318  cncfmet  22519  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  ply1divalg2  23702  nvm  26880  madjusmdetlem1  29221  xrge0pluscn  29314  esumpfinvallem  29463  ptrecube  32579  equivbnd2  32761  ismtyres  32777  iccbnd  32809  exidreslem  32846  iscrngo2  32966  toycom  33278  mendplusgfval  36774  sge0tsms  39273  vonn0ioo  39578  vonn0icc  39579  issubmgm  41579  rhmsubclem4  41881  zlmodzxzadd  41929  snlindsntor  42054