Theorem oveqi 7169

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  oveq123i  7170  cantnfval2  9132  vdwap1  16313  vdwlem12  16328  prdsdsval3  16758  oppchom  16985  rcaninv  17064  initoeu2lem0  17273  yonedalem21  17523  yonedalem22  17528  mndprop  17937  issubm  17968  frmdadd  18020  smndex1sgrp  18073  smndex1mnd  18075  grpprop  18119  oppgplus  18477  ablprop  18918  ringpropd  19332  crngpropd  19333  ringprop  19334  opprmul  19376  opprringb  19382  mulgass3  19387  rngidpropd  19445  invrpropd  19448  drngprop  19513  subrgpropd  19570  rhmpropd  19571  lidlacl  19986  lidlmcl  19990  lidlrsppropd  20003  crngridl  20011  psradd  20162  ressmpladd  20238  ressmplmul  20239  ressmplvsca  20240  ressply1add  20398  ressply1mul  20399  ressply1vsca  20400  ply1coe  20464  scmatscmiddistr  21117  1marepvsma1  21192  decpmatmulsumfsupp  21381  pmatcollpw1lem2  21383  pmatcollpwscmatlem1  21397  mptcoe1matfsupp  21410  mp2pm2mplem4  21417  chmatval  21437  chpidmat  21455  xpsdsval  22991  blres  23041  nmfval2  23200  nmval2  23201  ngpocelbl  23313  cncfmet  23516  ehl2eudisval  24026  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem6  24037  ply1divalg2  24732  clwwlknon1  27876  clwwlknon1nloop  27878  clwwlknon2  27881  nvm  28418  madjusmdetlem1  31092  xrge0pluscn  31183  esumpfinvallem  31333  ptrecube  34907  equivbnd2  35085  ismtyres  35101  iccbnd  35133  exidreslem  35170  iscrngo2  35290  toycom  36124  frlmsnic  39169  mendplusgfval  39805  sge0tsms  42682  vonn0ioo  42989  vonn0icc  42990  issubmgm  44076  rhmsubclem4  44380  zlmodzxzadd  44426  snlindsntor  44546