Theorem oveqi 7423

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413

This theorem is referenced by:  oveq123i  7424  fvmpopr2d  7574  cantnfval2  9688  vdwap1  17002  vdwlem12  17017  prdsdsval3  17504  oppchom  17732  rcaninv  17812  initoeu2lem0  18031  yonedalem21  18290  yonedalem22  18295  issubmgm  18685  mndprop  18743  issubm  18786  frmdadd  18838  smndex1sgrp  18891  smndex1mnd  18893  grpprop  18940  oppgplus  19337  ablprop  19779  ringpropd  20253  crngpropd  20254  ringprop  20255  opprmul  20305  opprrngb  20311  opprringb  20313  mulgass3  20318  rngidpropd  20380  invrpropd  20383  rhmimasubrng  20531  cntzsubrng  20532  subrngpropd  20533  subrgpropd  20573  rhmpropd  20574  rhmsubclem4  20653  drngprop  20709  lidlacl  21187  lidlrsppropd  21210  crngridl  21246  pzriprnglem5  21451  pzriprnglem6  21452  pzriprng1ALT  21462  psradd  21902  ressmpladd  21992  ressmplmul  21993  ressmplvsca  21994  ressply1add  22170  ressply1mul  22171  ressply1vsca  22172  ply1coe  22241  evls1addd  22314  evls1muld  22315  evls1vsca  22316  rhmply1  22329  rhmply1vsca  22331  scmatscmiddistr  22451  1marepvsma1  22526  decpmatmulsumfsupp  22716  pmatcollpw1lem2  22718  pmatcollpwscmatlem1  22732  mptcoe1matfsupp  22745  mp2pm2mplem4  22752  chmatval  22772  chpidmat  22790  xpsdsval  24325  blres  24375  nmfval0  24534  nmval2  24536  ngpocelbl  24648  cncfmet  24858  ehl2eudisval  25380  minveclem2  25383  minveclem3b  25385  minveclem4  25389  minveclem6  25391  ply1divalg2  26101  clwwlknon1  30083  clwwlknon1nloop  30085  clwwlknon2  30088  nvm  30627  opprqusplusg  33509  zringfrac  33574  evls1subd  33590  algextdeglem8  33763  madjusmdetlem1  33863  xrge0pluscn  33976  esumpfinvallem  34110  ptrecube  37649  equivbnd2  37821  ismtyres  37837  iccbnd  37869  exidreslem  37906  iscrngo2  38026  toycom  38996  aks6d1c1p5  42130  aks5lem3a  42207  frlmsnic  42530  mendplusgfval  43172  sge0tsms  46376  vonn0ioo  46683  vonn0icc  46684  zlmodzxzadd  48300  snlindsntor  48414  ovsng2  48802  isisod  48964  upeu2lem  48965  imaidfu  49036  cofuswapf2  49173  indthinc  49315  indthincALT  49316  prsthinc  49317