Theorem oveqi 7453

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  oveq123i  7454  fvmpopr2d  7603  ovmptss  8126  cantnfval2  9694  vdwap1  17181  vdwlem12  17196  prdsdsval3  17682  oppchom  17915  rcaninv  17995  initoeu2lem0  18214  yonedalem21  18473  yonedalem22  18478  mgmn0plusgf  18853  issubmgm  18917  mndprop  18978  issubm  19024  frmdadd  19077  smndex1sgrp  19133  smndex1mnd  19135  grpprop  19189  oppgplus  19590  ablprop  20034  ringpropd  20546  crngpropd  20547  ringprop  20548  opprmul  20597  opprrngb  20603  opprringb  20605  mulgass3  20610  rngidpropd  20672  invrpropd  20675  rhmimasubrng  20845  cntzsubrng  20846  subrngpropd  20847  subrgpropd  20887  rhmpropd  20888  rhmsubclem4  20967  drngprop  21025  isdrng3lem1  21032  lidlacl  21527  lidlrsppropd  21559  crngridl  21602  pzriprnglem5  21818  pzriprnglem6  21819  pzriprng1ALT  21829  psradd  22273  ressmpladd  22364  ressmplmul  22365  ressmplvsca  22366  ressply1add  22574  ressply1mul  22575  ressply1vsca  22576  ply1coe  22643  evls1addd  22716  evls1muld  22717  evls1vsca  22718  rhmply1  22728  rhmply1vsca  22730  scmatscmiddistr  22850  1marepvsma1  22925  decpmatmulsumfsupp  23118  pmatcollpw1lem2  23120  pmatcollpwscmatlem1  23134  mptcoe1matfsupp  23147  mp2pm2mplem4  23154  chmatval  23174  chpidmat  23192  xpsdsval  24727  blres  24777  nmfval0  24936  nmval2  24938  ngpocelbl  25050  cncfmet  25257  ehl2eudisval  25771  minveclem2  25774  minveclem3b  25776  minveclem4  25780  minveclem6  25782  ply1divalg2  26484  symquadmid  29331  prlngmid2  29466  clwwlknon1  30715  clwwlknon1nloop  30717  clwwlknon2  30720  nvm  31270  opprqusplusg  34080  zringfrac  34153  evls1subd  34171  algextdeglem8  34423  madjusmdetlem1  34526  xrge0pluscn  34639  esumpfinvallem  34773  ptrecube  38729  equivbnd2  38917  ismtyres  38933  iccbnd  38965  exidreslem  39002  iscrngo2  39122  toycom  40221  aks6d1c1p5  43353  aks5lem3a  43430  frlmsnic  43795  mendplusgfval  44373  sge0tsms  47593  vonn0ioo  47900  vonn0icc  47901  zlmodzxzadd  49673  snlindsntor  49786  ovsng2  50173  isisod  50344  upeu2lem  50345  imaidfu  50429  cofuswapf2  50620  indthinc  50800  indthincALT  50801  prsthinc  50802  lmddu  51053