Theorem oveqi 7429

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  oveq123i  7430  fvmpopr2d  7578  cantnfval2  9651  vdwap1  17073  vdwlem12  17088  prdsdsval3  17574  oppchom  17807  rcaninv  17887  initoeu2lem0  18106  yonedalem21  18365  yonedalem22  18370  mgmn0plusgf  18745  issubmgm  18806  mndprop  18867  issubm  18912  frmdadd  18965  smndex1sgrp  19021  smndex1mnd  19023  grpprop  19077  oppgplus  19477  ablprop  19921  ringpropd  20431  crngpropd  20432  ringprop  20433  opprmul  20482  opprrngb  20488  opprringb  20490  mulgass3  20495  rngidpropd  20557  invrpropd  20560  rhmimasubrng  20729  cntzsubrng  20730  subrngpropd  20731  subrgpropd  20771  rhmpropd  20772  rhmsubclem4  20851  drngprop  20908  isdrng3lem1  20915  lidlacl  21410  lidlrsppropd  21442  crngridl  21483  pzriprnglem5  21699  pzriprnglem6  21700  pzriprng1ALT  21710  psradd  22154  ressmpladd  22245  ressmplmul  22246  ressmplvsca  22247  ressply1add  22455  ressply1mul  22456  ressply1vsca  22457  ply1coe  22524  evls1addd  22597  evls1muld  22598  evls1vsca  22599  rhmply1  22609  rhmply1vsca  22611  scmatscmiddistr  22731  1marepvsma1  22806  decpmatmulsumfsupp  22999  pmatcollpw1lem2  23001  pmatcollpwscmatlem1  23015  mptcoe1matfsupp  23028  mp2pm2mplem4  23035  chmatval  23055  chpidmat  23073  xpsdsval  24608  blres  24658  nmfval0  24817  nmval2  24819  ngpocelbl  24931  cncfmet  25138  ehl2eudisval  25652  minveclem2  25655  minveclem3b  25657  minveclem4  25661  minveclem6  25663  ply1divalg2  26366  symquadmid  29181  prlngmid2  29304  clwwlknon1  30553  clwwlknon1nloop  30555  clwwlknon2  30558  nvm  31108  opprqusplusg  33878  zringfrac  33951  evls1subd  33969  algextdeglem8  34221  madjusmdetlem1  34324  xrge0pluscn  34437  esumpfinvallem  34571  ptrecube  38356  equivbnd2  38529  ismtyres  38545  iccbnd  38577  exidreslem  38614  iscrngo2  38734  toycom  39833  aks6d1c1p5  42965  aks5lem3a  43042  frlmsnic  43409  mendplusgfval  44009  sge0tsms  47195  vonn0ioo  47502  vonn0icc  47503  zlmodzxzadd  49275  snlindsntor  49388  ovsng2  49774  isisod  49940  upeu2lem  49941  imaidfu  50023  cofuswapf2  50208  indthinc  50375  indthincALT  50376  prsthinc  50377  lmddu  50580