Theorem oveqi 7422

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6484  df-fv 6536  df-ov 7412

This theorem is used by:  oveq123i  7423  fvmpopr2d  7571  cantnfval2  9648  vdwap1  17102  vdwlem12  17117  prdsdsval3  17603  oppchom  17836  rcaninv  17916  initoeu2lem0  18135  yonedalem21  18394  yonedalem22  18399  mgmn0plusgf  18774  issubmgm  18838  mndprop  18899  issubm  18945  frmdadd  18998  smndex1sgrp  19054  smndex1mnd  19056  grpprop  19110  oppgplus  19510  ablprop  19954  ringpropd  20466  crngpropd  20467  ringprop  20468  opprmul  20517  opprrngb  20523  opprringb  20525  mulgass3  20530  rngidpropd  20592  invrpropd  20595  rhmimasubrng  20765  cntzsubrng  20766  subrngpropd  20767  subrgpropd  20807  rhmpropd  20808  rhmsubclem4  20887  drngprop  20945  isdrng3lem1  20952  lidlacl  21447  lidlrsppropd  21479  crngridl  21522  pzriprnglem5  21738  pzriprnglem6  21739  pzriprng1ALT  21749  psradd  22193  ressmpladd  22284  ressmplmul  22285  ressmplvsca  22286  ressply1add  22494  ressply1mul  22495  ressply1vsca  22496  ply1coe  22563  evls1addd  22636  evls1muld  22637  evls1vsca  22638  rhmply1  22648  rhmply1vsca  22650  scmatscmiddistr  22770  1marepvsma1  22845  decpmatmulsumfsupp  23038  pmatcollpw1lem2  23040  pmatcollpwscmatlem1  23054  mptcoe1matfsupp  23067  mp2pm2mplem4  23074  chmatval  23094  chpidmat  23112  xpsdsval  24647  blres  24697  nmfval0  24856  nmval2  24858  ngpocelbl  24970  cncfmet  25177  ehl2eudisval  25691  minveclem2  25694  minveclem3b  25696  minveclem4  25700  minveclem6  25702  ply1divalg2  26404  symquadmid  29223  prlngmid2  29358  clwwlknon1  30607  clwwlknon1nloop  30609  clwwlknon2  30612  nvm  31162  opprqusplusg  33932  zringfrac  34005  evls1subd  34023  algextdeglem8  34275  madjusmdetlem1  34378  xrge0pluscn  34491  esumpfinvallem  34625  ptrecube  38452  equivbnd2  38640  ismtyres  38656  iccbnd  38688  exidreslem  38725  iscrngo2  38845  toycom  39944  aks6d1c1p5  43076  aks5lem3a  43153  frlmsnic  43520  mendplusgfval  44120  sge0tsms  47306  vonn0ioo  47613  vonn0icc  47614  zlmodzxzadd  49386  snlindsntor  49499  ovsng2  49885  isisod  50051  upeu2lem  50052  imaidfu  50134  cofuswapf2  50319  indthinc  50486  indthincALT  50487  prsthinc  50488  lmddu  50691