Theorem oveqi 7380

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

Syntax hints:   = wceq 1542  (class class class)co 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  oveq123i  7381  fvmpopr2d  7529  cantnfval2  9590  vdwap1  16948  vdwlem12  16963  prdsdsval3  17448  oppchom  17681  rcaninv  17761  initoeu2lem0  17980  yonedalem21  18239  yonedalem22  18244  issubmgm  18670  mndprop  18728  issubm  18771  frmdadd  18823  smndex1sgrp  18879  smndex1mnd  18881  grpprop  18928  oppgplus  19324  ablprop  19768  ringpropd  20269  crngpropd  20270  ringprop  20271  opprmul  20320  opprrngb  20326  opprringb  20328  mulgass3  20333  rngidpropd  20395  invrpropd  20398  rhmimasubrng  20543  cntzsubrng  20544  subrngpropd  20545  subrgpropd  20585  rhmpropd  20586  rhmsubclem4  20665  drngprop  20721  lidlacl  21219  lidlrsppropd  21242  crngridl  21278  pzriprnglem5  21465  pzriprnglem6  21466  pzriprng1ALT  21476  psradd  21917  ressmpladd  22007  ressmplmul  22008  ressmplvsca  22009  ressply1add  22193  ressply1mul  22194  ressply1vsca  22195  ply1coe  22263  evls1addd  22336  evls1muld  22337  evls1vsca  22338  rhmply1  22351  rhmply1vsca  22353  scmatscmiddistr  22473  1marepvsma1  22548  decpmatmulsumfsupp  22738  pmatcollpw1lem2  22740  pmatcollpwscmatlem1  22754  mptcoe1matfsupp  22767  mp2pm2mplem4  22774  chmatval  22794  chpidmat  22812  xpsdsval  24346  blres  24396  nmfval0  24555  nmval2  24557  ngpocelbl  24669  cncfmet  24876  ehl2eudisval  25390  minveclem2  25393  minveclem3b  25395  minveclem4  25399  minveclem6  25401  ply1divalg2  26104  clwwlknon1  30167  clwwlknon1nloop  30169  clwwlknon2  30172  nvm  30712  opprqusplusg  33549  zringfrac  33614  evls1subd  33632  algextdeglem8  33868  madjusmdetlem1  33971  xrge0pluscn  34084  esumpfinvallem  34218  ptrecube  37941  equivbnd2  38113  ismtyres  38129  iccbnd  38161  exidreslem  38198  iscrngo2  38318  toycom  39419  aks6d1c1p5  42551  aks5lem3a  42628  frlmsnic  42985  mendplusgfval  43609  sge0tsms  46808  vonn0ioo  47115  vonn0icc  47116  zlmodzxzadd  48834  snlindsntor  48947  ovsng2  49334  isisod  49502  upeu2lem  49503  imaidfu  49585  cofuswapf2  49770  indthinc  49937  indthincALT  49938  prsthinc  49939  lmddu  50142