Theorem oveqi 7373

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  oveq123i  7374  fvmpopr2d  7522  cantnfval2  9582  vdwap1  16909  vdwlem12  16924  prdsdsval3  17409  oppchom  17642  rcaninv  17722  initoeu2lem0  17941  yonedalem21  18200  yonedalem22  18205  issubmgm  18631  mndprop  18689  issubm  18732  frmdadd  18784  smndex1sgrp  18837  smndex1mnd  18839  grpprop  18886  oppgplus  19282  ablprop  19726  ringpropd  20227  crngpropd  20228  ringprop  20229  opprmul  20280  opprrngb  20286  opprringb  20288  mulgass3  20293  rngidpropd  20355  invrpropd  20358  rhmimasubrng  20503  cntzsubrng  20504  subrngpropd  20505  subrgpropd  20545  rhmpropd  20546  rhmsubclem4  20625  drngprop  20681  lidlacl  21180  lidlrsppropd  21203  crngridl  21239  pzriprnglem5  21444  pzriprnglem6  21445  pzriprng1ALT  21455  psradd  21897  ressmpladd  21988  ressmplmul  21989  ressmplvsca  21990  ressply1add  22174  ressply1mul  22175  ressply1vsca  22176  ply1coe  22246  evls1addd  22319  evls1muld  22320  evls1vsca  22321  rhmply1  22334  rhmply1vsca  22336  scmatscmiddistr  22456  1marepvsma1  22531  decpmatmulsumfsupp  22721  pmatcollpw1lem2  22723  pmatcollpwscmatlem1  22737  mptcoe1matfsupp  22750  mp2pm2mplem4  22757  chmatval  22777  chpidmat  22795  xpsdsval  24329  blres  24379  nmfval0  24538  nmval2  24540  ngpocelbl  24652  cncfmet  24862  ehl2eudisval  25383  minveclem2  25386  minveclem3b  25388  minveclem4  25392  minveclem6  25394  ply1divalg2  26104  clwwlknon1  30176  clwwlknon1nloop  30178  clwwlknon2  30181  nvm  30720  opprqusplusg  33572  zringfrac  33637  evls1subd  33655  algextdeglem8  33883  madjusmdetlem1  33986  xrge0pluscn  34099  esumpfinvallem  34233  ptrecube  37823  equivbnd2  37995  ismtyres  38011  iccbnd  38043  exidreslem  38080  iscrngo2  38200  toycom  39301  aks6d1c1p5  42434  aks5lem3a  42511  frlmsnic  42862  mendplusgfval  43490  sge0tsms  46691  vonn0ioo  46998  vonn0icc  46999  zlmodzxzadd  48671  snlindsntor  48784  ovsng2  49171  isisod  49339  upeu2lem  49340  imaidfu  49422  cofuswapf2  49607  indthinc  49774  indthincALT  49775  prsthinc  49776  lmddu  49979