Theorem oveqi 6923

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

Syntax hints:   = wceq 1656  (class class class)co 6910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-uni 4661  df-br 4876  df-iota 6090  df-fv 6135  df-ov 6913

This theorem is referenced by:  oveq123i  6924  cantnfval2  8850  vdwap1  16059  vdwlem12  16074  prdsdsval3  16505  oppchom  16734  rcaninv  16813  initoeu2lem0  17022  yonedalem21  17273  yonedalem22  17278  mndprop  17677  issubm  17707  frmdadd  17753  grpprop  17799  oppgplus  18136  ablprop  18564  ringpropd  18943  crngpropd  18944  ringprop  18945  opprmul  18987  opprringb  18993  mulgass3  18998  rngidpropd  19056  invrpropd  19059  drngprop  19121  subrgpropd  19177  rhmpropd  19178  lidlacl  19581  lidlmcl  19585  lidlrsppropd  19598  crngridl  19606  psradd  19750  ressmpladd  19825  ressmplmul  19826  ressmplvsca  19827  ressply1add  19967  ressply1mul  19968  ressply1vsca  19969  ply1coe  20033  scmatscmiddistr  20689  1marepvsma1  20764  decpmatmulsumfsupp  20955  pmatcollpw1lem2  20957  pmatcollpwscmatlem1  20971  mptcoe1matfsupp  20984  mp2pm2mplem4  20991  chmatval  21011  chpidmat  21029  xpsdsval  22563  blres  22613  nmfval2  22772  nmval2  22773  ngpocelbl  22885  cncfmet  23088  ehl1eudisval  23596  ehl2eudisval  23598  minveclem2  23601  minveclem3b  23603  minveclem4  23607  minveclem6  23609  ply1divalg2  24304  clwwlknon1  27468  clwwlknon1nloop  27470  clwwlknon2  27473  nvm  28047  madjusmdetlem1  30434  xrge0pluscn  30527  esumpfinvallem  30677  ptrecube  33952  equivbnd2  34132  ismtyres  34148  iccbnd  34180  exidreslem  34217  iscrngo2  34337  toycom  35047  mendplusgfval  38597  sge0tsms  41386  vonn0ioo  41693  vonn0icc  41694  issubmgm  42654  rhmsubclem4  42954  zlmodzxzadd  43001  snlindsntor  43125