Theorem oveqi 7371

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

Syntax hints:   = wceq 1542  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863  df-br 5098  df-iota 6447  df-fv 6499  df-ov 7361

This theorem is referenced by:  oveq123i  7372  fvmpopr2d  7520  cantnfval2  9580  vdwap1  16907  vdwlem12  16922  prdsdsval3  17407  oppchom  17640  rcaninv  17720  initoeu2lem0  17939  yonedalem21  18198  yonedalem22  18203  issubmgm  18629  mndprop  18687  issubm  18730  frmdadd  18782  smndex1sgrp  18835  smndex1mnd  18837  grpprop  18884  oppgplus  19280  ablprop  19724  ringpropd  20225  crngpropd  20226  ringprop  20227  opprmul  20278  opprrngb  20284  opprringb  20286  mulgass3  20291  rngidpropd  20353  invrpropd  20356  rhmimasubrng  20501  cntzsubrng  20502  subrngpropd  20503  subrgpropd  20543  rhmpropd  20544  rhmsubclem4  20623  drngprop  20679  lidlacl  21178  lidlrsppropd  21201  crngridl  21237  pzriprnglem5  21442  pzriprnglem6  21443  pzriprng1ALT  21453  psradd  21895  ressmpladd  21986  ressmplmul  21987  ressmplvsca  21988  ressply1add  22172  ressply1mul  22173  ressply1vsca  22174  ply1coe  22244  evls1addd  22317  evls1muld  22318  evls1vsca  22319  rhmply1  22332  rhmply1vsca  22334  scmatscmiddistr  22454  1marepvsma1  22529  decpmatmulsumfsupp  22719  pmatcollpw1lem2  22721  pmatcollpwscmatlem1  22735  mptcoe1matfsupp  22748  mp2pm2mplem4  22755  chmatval  22775  chpidmat  22793  xpsdsval  24327  blres  24377  nmfval0  24536  nmval2  24538  ngpocelbl  24650  cncfmet  24860  ehl2eudisval  25381  minveclem2  25384  minveclem3b  25386  minveclem4  25390  minveclem6  25392  ply1divalg2  26102  clwwlknon1  30153  clwwlknon1nloop  30155  clwwlknon2  30158  nvm  30697  opprqusplusg  33549  zringfrac  33614  evls1subd  33632  algextdeglem8  33860  madjusmdetlem1  33963  xrge0pluscn  34076  esumpfinvallem  34210  ptrecube  37790  equivbnd2  37962  ismtyres  37978  iccbnd  38010  exidreslem  38047  iscrngo2  38167  toycom  39268  aks6d1c1p5  42401  aks5lem3a  42478  frlmsnic  42832  mendplusgfval  43460  sge0tsms  46661  vonn0ioo  46968  vonn0icc  46969  zlmodzxzadd  48641  snlindsntor  48754  ovsng2  49141  isisod  49309  upeu2lem  49310  imaidfu  49392  cofuswapf2  49577  indthinc  49744  indthincALT  49745  prsthinc  49746  lmddu  49949