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 ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  oveq123i  7434  fvmpopr2d  7582  cantnfval2  9670  vdwap1  17155  vdwlem12  17170  prdsdsval3  17656  oppchom  17889  rcaninv  17969  initoeu2lem0  18188  yonedalem21  18447  yonedalem22  18452  mgmn0plusgf  18827  issubmgm  18891  mndprop  18952  issubm  18998  frmdadd  19051  smndex1sgrp  19107  smndex1mnd  19109  grpprop  19163  oppgplus  19563  ablprop  20007  ringpropd  20519  crngpropd  20520  ringprop  20521  opprmul  20570  opprrngb  20576  opprringb  20578  mulgass3  20583  rngidpropd  20645  invrpropd  20648  rhmimasubrng  20818  cntzsubrng  20819  subrngpropd  20820  subrgpropd  20860  rhmpropd  20861  rhmsubclem4  20940  drngprop  20998  isdrng3lem1  21005  lidlacl  21500  lidlrsppropd  21532  crngridl  21575  pzriprnglem5  21791  pzriprnglem6  21792  pzriprng1ALT  21802  psradd  22246  ressmpladd  22337  ressmplmul  22338  ressmplvsca  22339  ressply1add  22547  ressply1mul  22548  ressply1vsca  22549  ply1coe  22616  evls1addd  22689  evls1muld  22690  evls1vsca  22691  rhmply1  22701  rhmply1vsca  22703  scmatscmiddistr  22823  1marepvsma1  22898  decpmatmulsumfsupp  23091  pmatcollpw1lem2  23093  pmatcollpwscmatlem1  23107  mptcoe1matfsupp  23120  mp2pm2mplem4  23127  chmatval  23147  chpidmat  23165  xpsdsval  24700  blres  24750  nmfval0  24909  nmval2  24911  ngpocelbl  25023  cncfmet  25230  ehl2eudisval  25744  minveclem2  25747  minveclem3b  25749  minveclem4  25753  minveclem6  25755  ply1divalg2  26457  symquadmid  29304  prlngmid2  29439  clwwlknon1  30688  clwwlknon1nloop  30690  clwwlknon2  30693  nvm  31243  opprqusplusg  34013  zringfrac  34086  evls1subd  34104  algextdeglem8  34356  madjusmdetlem1  34459  xrge0pluscn  34572  esumpfinvallem  34706  ptrecube  38539  equivbnd2  38727  ismtyres  38743  iccbnd  38775  exidreslem  38812  iscrngo2  38932  toycom  40031  aks6d1c1p5  43163  aks5lem3a  43240  frlmsnic  43605  mendplusgfval  44183  sge0tsms  47390  vonn0ioo  47697  vonn0icc  47698  zlmodzxzadd  49470  snlindsntor  49583  ovsng2  49969  isisod  50135  upeu2lem  50136  imaidfu  50218  cofuswapf2  50403  indthinc  50570  indthincALT  50571  prsthinc  50572  lmddu  50775