Theorem oveqi 7461

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

Syntax hints:   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  oveq123i  7462  fvmpopr2d  7612  cantnfval2  9738  vdwap1  17024  vdwlem12  17039  prdsdsval3  17545  oppchom  17774  rcaninv  17855  initoeu2lem0  18080  yonedalem21  18343  yonedalem22  18348  issubmgm  18740  mndprop  18798  issubm  18838  frmdadd  18890  smndex1sgrp  18943  smndex1mnd  18945  grpprop  18992  oppgplus  19389  ablprop  19835  ringpropd  20311  crngpropd  20312  ringprop  20313  opprmul  20363  opprrngb  20372  opprringb  20374  mulgass3  20379  rngidpropd  20441  invrpropd  20444  rhmimasubrng  20592  cntzsubrng  20593  subrngpropd  20594  subrgpropd  20636  rhmpropd  20637  rhmsubclem4  20710  drngprop  20766  lidlacl  21254  lidlrsppropd  21277  crngridl  21313  pzriprnglem5  21519  pzriprnglem6  21520  pzriprng1ALT  21530  psradd  21980  ressmpladd  22070  ressmplmul  22071  ressmplvsca  22072  ressply1add  22252  ressply1mul  22253  ressply1vsca  22254  ply1coe  22323  evls1addd  22396  evls1muld  22397  evls1vsca  22398  rhmply1  22411  rhmply1vsca  22413  scmatscmiddistr  22535  1marepvsma1  22610  decpmatmulsumfsupp  22800  pmatcollpw1lem2  22802  pmatcollpwscmatlem1  22816  mptcoe1matfsupp  22829  mp2pm2mplem4  22836  chmatval  22856  chpidmat  22874  xpsdsval  24412  blres  24462  nmfval0  24624  nmval2  24626  ngpocelbl  24746  cncfmet  24954  ehl2eudisval  25476  minveclem2  25479  minveclem3b  25481  minveclem4  25485  minveclem6  25487  ply1divalg2  26198  clwwlknon1  30129  clwwlknon1nloop  30131  clwwlknon2  30134  nvm  30673  opprqusplusg  33482  zringfrac  33547  evls1subd  33562  algextdeglem8  33715  madjusmdetlem1  33773  xrge0pluscn  33886  esumpfinvallem  34038  ptrecube  37580  equivbnd2  37752  ismtyres  37768  iccbnd  37800  exidreslem  37837  iscrngo2  37957  toycom  38929  aks6d1c1p5  42069  aks5lem3a  42146  frlmsnic  42495  mendplusgfval  43142  sge0tsms  46301  vonn0ioo  46608  vonn0icc  46609  zlmodzxzadd  48083  snlindsntor  48200  indthinc  48719  indthincALT  48720  prsthinc  48721  mndtchom  48757