Theorem oveqi 7400

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

Syntax hints:   = wceq 1540  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  oveq123i  7401  fvmpopr2d  7551  cantnfval2  9622  vdwap1  16948  vdwlem12  16963  prdsdsval3  17448  oppchom  17676  rcaninv  17756  initoeu2lem0  17975  yonedalem21  18234  yonedalem22  18239  issubmgm  18629  mndprop  18687  issubm  18730  frmdadd  18782  smndex1sgrp  18835  smndex1mnd  18837  grpprop  18884  oppgplus  19281  ablprop  19723  ringpropd  20197  crngpropd  20198  ringprop  20199  opprmul  20249  opprrngb  20255  opprringb  20257  mulgass3  20262  rngidpropd  20324  invrpropd  20327  rhmimasubrng  20475  cntzsubrng  20476  subrngpropd  20477  subrgpropd  20517  rhmpropd  20518  rhmsubclem4  20597  drngprop  20653  lidlacl  21131  lidlrsppropd  21154  crngridl  21190  pzriprnglem5  21395  pzriprnglem6  21396  pzriprng1ALT  21406  psradd  21846  ressmpladd  21936  ressmplmul  21937  ressmplvsca  21938  ressply1add  22114  ressply1mul  22115  ressply1vsca  22116  ply1coe  22185  evls1addd  22258  evls1muld  22259  evls1vsca  22260  rhmply1  22273  rhmply1vsca  22275  scmatscmiddistr  22395  1marepvsma1  22470  decpmatmulsumfsupp  22660  pmatcollpw1lem2  22662  pmatcollpwscmatlem1  22676  mptcoe1matfsupp  22689  mp2pm2mplem4  22696  chmatval  22716  chpidmat  22734  xpsdsval  24269  blres  24319  nmfval0  24478  nmval2  24480  ngpocelbl  24592  cncfmet  24802  ehl2eudisval  25323  minveclem2  25326  minveclem3b  25328  minveclem4  25332  minveclem6  25334  ply1divalg2  26044  clwwlknon1  30026  clwwlknon1nloop  30028  clwwlknon2  30031  nvm  30570  opprqusplusg  33460  zringfrac  33525  evls1subd  33541  algextdeglem8  33714  madjusmdetlem1  33817  xrge0pluscn  33930  esumpfinvallem  34064  ptrecube  37614  equivbnd2  37786  ismtyres  37802  iccbnd  37834  exidreslem  37871  iscrngo2  37991  toycom  38966  aks6d1c1p5  42100  aks5lem3a  42177  frlmsnic  42528  mendplusgfval  43170  sge0tsms  46378  vonn0ioo  46685  vonn0icc  46686  zlmodzxzadd  48343  snlindsntor  48457  ovsng2  48844  isisod  49013  upeu2lem  49014  imaidfu  49096  cofuswapf2  49281  indthinc  49448  indthincALT  49449  prsthinc  49450  lmddu  49653