Theorem oveqi 7195

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-in 3860  df-ss 3870  df-uni 4807  df-br 5041  df-iota 6307  df-fv 6357  df-ov 7185

This theorem is referenced by:  oveq123i  7196  fvmpopr2d  7338  cantnfval2  9217  vdwap1  16425  vdwlem12  16440  prdsdsval3  16873  oppchom  17101  rcaninv  17181  initoeu2lem0  17397  yonedalem21  17651  yonedalem22  17656  mndprop  18065  issubm  18096  frmdadd  18148  smndex1sgrp  18201  smndex1mnd  18203  grpprop  18249  oppgplus  18607  ablprop  19048  ringpropd  19466  crngpropd  19467  ringprop  19468  opprmul  19510  opprringb  19516  mulgass3  19521  rngidpropd  19579  invrpropd  19582  drngprop  19644  subrgpropd  19701  rhmpropd  19702  lidlacl  20117  lidlmcl  20121  lidlrsppropd  20134  crngridl  20142  psradd  20773  ressmpladd  20852  ressmplmul  20853  ressmplvsca  20854  ressply1add  21017  ressply1mul  21018  ressply1vsca  21019  ply1coe  21083  scmatscmiddistr  21271  1marepvsma1  21346  decpmatmulsumfsupp  21536  pmatcollpw1lem2  21538  pmatcollpwscmatlem1  21552  mptcoe1matfsupp  21565  mp2pm2mplem4  21572  chmatval  21592  chpidmat  21610  xpsdsval  23146  blres  23196  nmfval0  23355  nmval2  23357  ngpocelbl  23469  cncfmet  23673  ehl2eudisval  24187  minveclem2  24190  minveclem3b  24192  minveclem4  24196  minveclem6  24198  ply1divalg2  24903  clwwlknon1  28046  clwwlknon1nloop  28048  clwwlknon2  28051  nvm  28588  madjusmdetlem1  31361  xrge0pluscn  31474  esumpfinvallem  31624  ptrecube  35432  equivbnd2  35605  ismtyres  35621  iccbnd  35653  exidreslem  35690  iscrngo2  35810  toycom  36642  frlmsnic  39884  mendplusgfval  40622  sge0tsms  43500  vonn0ioo  43807  vonn0icc  43808  issubmgm  44924  rhmsubclem4  45228  zlmodzxzadd  45275  snlindsntor  45393  indthinc  45844  indthincALT  45845  prsthinc  45846  mndtchom  45871