Theorem oveqi 7425

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415

This theorem is used by:  oveq123i  7426  fvmpopr2d  7574  cantnfval2  9636  vdwap1  17043  vdwlem12  17058  prdsdsval3  17544  oppchom  17777  rcaninv  17857  initoeu2lem0  18076  yonedalem21  18335  yonedalem22  18340  issubmgm  18766  mndprop  18824  issubm  18867  frmdadd  18920  smndex1sgrp  18976  smndex1mnd  18978  grpprop  19025  oppgplus  19425  ablprop  19869  ringpropd  20378  crngpropd  20379  ringprop  20380  opprmul  20429  opprrngb  20435  opprringb  20437  mulgass3  20442  rngidpropd  20504  invrpropd  20507  rhmimasubrng  20676  cntzsubrng  20677  subrngpropd  20678  subrgpropd  20718  rhmpropd  20719  rhmsubclem4  20798  drngprop  20855  isdrng3lem1  20862  lidlacl  21357  lidlrsppropd  21389  crngridl  21430  pzriprnglem5  21646  pzriprnglem6  21647  pzriprng1ALT  21657  psradd  22099  ressmpladd  22190  ressmplmul  22191  ressmplvsca  22192  ressply1add  22400  ressply1mul  22401  ressply1vsca  22402  ply1coe  22469  evls1addd  22542  evls1muld  22543  evls1vsca  22544  rhmply1  22554  rhmply1vsca  22556  scmatscmiddistr  22676  1marepvsma1  22751  decpmatmulsumfsupp  22941  pmatcollpw1lem2  22943  pmatcollpwscmatlem1  22957  mptcoe1matfsupp  22970  mp2pm2mplem4  22977  chmatval  22997  chpidmat  23015  xpsdsval  24549  blres  24599  nmfval0  24758  nmval2  24760  ngpocelbl  24872  cncfmet  25079  ehl2eudisval  25593  minveclem2  25596  minveclem3b  25598  minveclem4  25602  minveclem6  25604  ply1divalg2  26307  symquadmid  29119  prlngmid2  29222  clwwlknon1  30459  clwwlknon1nloop  30461  clwwlknon2  30464  nvm  31004  opprqusplusg  33780  zringfrac  33853  evls1subd  33871  algextdeglem8  34123  madjusmdetlem1  34226  xrge0pluscn  34339  esumpfinvallem  34473  ptrecube  38299  equivbnd2  38471  ismtyres  38487  iccbnd  38519  exidreslem  38556  iscrngo2  38676  toycom  39775  aks6d1c1p5  42907  aks5lem3a  42984  frlmsnic  43336  mendplusgfval  43936  sge0tsms  47122  vonn0ioo  47429  vonn0icc  47430  zlmodzxzadd  49166  snlindsntor  49279  ovsng2  49665  isisod  49833  upeu2lem  49834  imaidfu  49916  cofuswapf2  50101  indthinc  50268  indthincALT  50269  prsthinc  50270  lmddu  50473  crosspdot0i  50672