Theorem oveqi 7297

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

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  oveq123i  7298  fvmpopr2d  7443  cantnfval2  9436  vdwap1  16687  vdwlem12  16702  prdsdsval3  17205  oppchom  17434  rcaninv  17515  initoeu2lem0  17737  yonedalem21  18000  yonedalem22  18005  mndprop  18420  issubm  18451  frmdadd  18503  smndex1sgrp  18556  smndex1mnd  18558  grpprop  18604  oppgplus  18962  ablprop  19407  ringpropd  19830  crngpropd  19831  ringprop  19832  opprmul  19874  opprringb  19883  mulgass3  19888  rngidpropd  19946  invrpropd  19949  drngprop  20011  subrgpropd  20068  rhmpropd  20069  lidlacl  20493  lidlmcl  20497  lidlrsppropd  20510  crngridl  20518  psradd  21160  ressmpladd  21239  ressmplmul  21240  ressmplvsca  21241  ressply1add  21410  ressply1mul  21411  ressply1vsca  21412  ply1coe  21476  scmatscmiddistr  21666  1marepvsma1  21741  decpmatmulsumfsupp  21931  pmatcollpw1lem2  21933  pmatcollpwscmatlem1  21947  mptcoe1matfsupp  21960  mp2pm2mplem4  21967  chmatval  21987  chpidmat  22005  xpsdsval  23543  blres  23593  nmfval0  23755  nmval2  23757  ngpocelbl  23877  cncfmet  24081  ehl2eudisval  24596  minveclem2  24599  minveclem3b  24601  minveclem4  24605  minveclem6  24607  ply1divalg2  25312  clwwlknon1  28470  clwwlknon1nloop  28472  clwwlknon2  28475  nvm  29012  madjusmdetlem1  31786  xrge0pluscn  31899  esumpfinvallem  32051  ptrecube  35786  equivbnd2  35959  ismtyres  35975  iccbnd  36007  exidreslem  36044  iscrngo2  36164  toycom  36994  frlmsnic  40270  mendplusgfval  41017  sge0tsms  43925  vonn0ioo  44232  vonn0icc  44233  issubmgm  45354  rhmsubclem4  45658  zlmodzxzadd  45705  snlindsntor  45823  indthinc  46344  indthincALT  46345  prsthinc  46346  mndtchom  46382