Theorem oveqi 7433

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

Syntax hints:   = wceq 1534  (class class class)co 7420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423

This theorem is referenced by:  oveq123i  7434  fvmpopr2d  7583  cantnfval2  9693  vdwap1  16946  vdwlem12  16961  prdsdsval3  17467  oppchom  17696  rcaninv  17777  initoeu2lem0  18002  yonedalem21  18265  yonedalem22  18270  issubmgm  18662  mndprop  18720  issubm  18755  frmdadd  18807  smndex1sgrp  18860  smndex1mnd  18862  grpprop  18909  oppgplus  19300  ablprop  19748  ringpropd  20224  crngpropd  20225  ringprop  20226  opprmul  20276  opprrngb  20285  opprringb  20287  mulgass3  20292  rngidpropd  20354  invrpropd  20357  rhmimasubrng  20503  cntzsubrng  20504  subrngpropd  20505  subrgpropd  20547  rhmpropd  20548  rhmsubclem4  20621  drngprop  20639  lidlacl  21117  lidlrsppropd  21139  crngridl  21172  pzriprnglem5  21411  pzriprnglem6  21412  pzriprng1ALT  21422  psradd  21882  ressmpladd  21967  ressmplmul  21968  ressmplvsca  21969  ressply1add  22148  ressply1mul  22149  ressply1vsca  22150  ply1coe  22217  evls1addd  22290  evls1muld  22291  evls1vsca  22292  scmatscmiddistr  22423  1marepvsma1  22498  decpmatmulsumfsupp  22688  pmatcollpw1lem2  22690  pmatcollpwscmatlem1  22704  mptcoe1matfsupp  22717  mp2pm2mplem4  22724  chmatval  22744  chpidmat  22762  xpsdsval  24300  blres  24350  nmfval0  24512  nmval2  24514  ngpocelbl  24634  cncfmet  24842  ehl2eudisval  25364  minveclem2  25367  minveclem3b  25369  minveclem4  25373  minveclem6  25375  ply1divalg2  26087  clwwlknon1  29920  clwwlknon1nloop  29922  clwwlknon2  29925  nvm  30464  zringfrac  33009  opprqusplusg  33213  evls1subd  33256  algextdeglem8  33392  madjusmdetlem1  33428  xrge0pluscn  33541  esumpfinvallem  33693  ptrecube  37093  equivbnd2  37265  ismtyres  37281  iccbnd  37313  exidreslem  37350  iscrngo2  37470  toycom  38445  aks6d1c1p5  41583  frlmsnic  41770  mendplusgfval  42609  sge0tsms  45768  vonn0ioo  46075  vonn0icc  46076  zlmodzxzadd  47422  snlindsntor  47539  indthinc  48058  indthincALT  48059  prsthinc  48060  mndtchom  48096