Theorem oveqi 7444

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

Syntax hints:   = wceq 1537  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434

This theorem is referenced by:  oveq123i  7445  fvmpopr2d  7595  cantnfval2  9707  vdwap1  17011  vdwlem12  17026  prdsdsval3  17532  oppchom  17761  rcaninv  17842  initoeu2lem0  18067  yonedalem21  18330  yonedalem22  18335  issubmgm  18728  mndprop  18786  issubm  18829  frmdadd  18881  smndex1sgrp  18934  smndex1mnd  18936  grpprop  18983  oppgplus  19380  ablprop  19826  ringpropd  20302  crngpropd  20303  ringprop  20304  opprmul  20354  opprrngb  20363  opprringb  20365  mulgass3  20370  rngidpropd  20432  invrpropd  20435  rhmimasubrng  20583  cntzsubrng  20584  subrngpropd  20585  subrgpropd  20625  rhmpropd  20626  rhmsubclem4  20705  drngprop  20761  lidlacl  21249  lidlrsppropd  21272  crngridl  21308  pzriprnglem5  21514  pzriprnglem6  21515  pzriprng1ALT  21525  psradd  21975  ressmpladd  22065  ressmplmul  22066  ressmplvsca  22067  ressply1add  22247  ressply1mul  22248  ressply1vsca  22249  ply1coe  22318  evls1addd  22391  evls1muld  22392  evls1vsca  22393  rhmply1  22406  rhmply1vsca  22408  scmatscmiddistr  22530  1marepvsma1  22605  decpmatmulsumfsupp  22795  pmatcollpw1lem2  22797  pmatcollpwscmatlem1  22811  mptcoe1matfsupp  22824  mp2pm2mplem4  22831  chmatval  22851  chpidmat  22869  xpsdsval  24407  blres  24457  nmfval0  24619  nmval2  24621  ngpocelbl  24741  cncfmet  24949  ehl2eudisval  25471  minveclem2  25474  minveclem3b  25476  minveclem4  25480  minveclem6  25482  ply1divalg2  26193  clwwlknon1  30126  clwwlknon1nloop  30128  clwwlknon2  30131  nvm  30670  opprqusplusg  33497  zringfrac  33562  evls1subd  33577  algextdeglem8  33730  madjusmdetlem1  33788  xrge0pluscn  33901  esumpfinvallem  34055  ptrecube  37607  equivbnd2  37779  ismtyres  37795  iccbnd  37827  exidreslem  37864  iscrngo2  37984  toycom  38955  aks6d1c1p5  42094  aks5lem3a  42171  frlmsnic  42527  mendplusgfval  43170  sge0tsms  46336  vonn0ioo  46643  vonn0icc  46644  zlmodzxzadd  48203  snlindsntor  48317  isisod  48807  upeu2lem  48808  indthinc  48853  indthincALT  48854  prsthinc  48855  mndtchom  48893