Theorem oveqi 7419

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  oveq123i  7420  fvmpopr2d  7566  cantnfval2  9661  vdwap1  16907  vdwlem12  16922  prdsdsval3  17428  oppchom  17657  rcaninv  17738  initoeu2lem0  17960  yonedalem21  18223  yonedalem22  18228  mndprop  18648  issubm  18681  frmdadd  18733  smndex1sgrp  18786  smndex1mnd  18788  grpprop  18835  oppgplus  19208  ablprop  19656  ringpropd  20096  crngpropd  20097  ringprop  20098  opprmul  20146  opprringb  20155  mulgass3  20160  rngidpropd  20222  invrpropd  20225  drngprop  20323  subrgpropd  20393  rhmpropd  20394  lidlacl  20829  lidlmcl  20833  lidlrsppropd  20848  crngridl  20869  psradd  21493  ressmpladd  21576  ressmplmul  21577  ressmplvsca  21578  ressply1add  21744  ressply1mul  21745  ressply1vsca  21746  ply1coe  21812  scmatscmiddistr  22002  1marepvsma1  22077  decpmatmulsumfsupp  22267  pmatcollpw1lem2  22269  pmatcollpwscmatlem1  22283  mptcoe1matfsupp  22296  mp2pm2mplem4  22303  chmatval  22323  chpidmat  22341  xpsdsval  23879  blres  23929  nmfval0  24091  nmval2  24093  ngpocelbl  24213  cncfmet  24417  ehl2eudisval  24932  minveclem2  24935  minveclem3b  24937  minveclem4  24941  minveclem6  24943  ply1divalg2  25648  clwwlknon1  29340  clwwlknon1nloop  29342  clwwlknon2  29345  nvm  29882  opprqusplusg  32592  evls1addd  32637  evls1muld  32638  evls1vsca  32639  madjusmdetlem1  32796  xrge0pluscn  32909  esumpfinvallem  33061  ptrecube  36477  equivbnd2  36649  ismtyres  36665  iccbnd  36697  exidreslem  36734  iscrngo2  36854  toycom  37832  frlmsnic  41108  mendplusgfval  41913  sge0tsms  45083  vonn0ioo  45390  vonn0icc  45391  issubmgm  46546  opprrngb  46662  rhmimasubrng  46730  cntzsubrng  46731  subrngpropd  46732  rhmsubclem4  46941  zlmodzxzadd  46988  snlindsntor  47106  indthinc  47626  indthincALT  47627  prsthinc  47628  mndtchom  47664