Theorem oveqi 7445

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

Syntax hints:   = wceq 1539  (class class class)co 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435

This theorem is referenced by:  oveq123i  7446  fvmpopr2d  7596  cantnfval2  9710  vdwap1  17016  vdwlem12  17031  prdsdsval3  17531  oppchom  17759  rcaninv  17839  initoeu2lem0  18059  yonedalem21  18319  yonedalem22  18324  issubmgm  18716  mndprop  18774  issubm  18817  frmdadd  18869  smndex1sgrp  18922  smndex1mnd  18924  grpprop  18971  oppgplus  19368  ablprop  19812  ringpropd  20286  crngpropd  20287  ringprop  20288  opprmul  20338  opprrngb  20347  opprringb  20349  mulgass3  20354  rngidpropd  20416  invrpropd  20419  rhmimasubrng  20567  cntzsubrng  20568  subrngpropd  20569  subrgpropd  20609  rhmpropd  20610  rhmsubclem4  20689  drngprop  20745  lidlacl  21232  lidlrsppropd  21255  crngridl  21291  pzriprnglem5  21497  pzriprnglem6  21498  pzriprng1ALT  21508  psradd  21958  ressmpladd  22048  ressmplmul  22049  ressmplvsca  22050  ressply1add  22232  ressply1mul  22233  ressply1vsca  22234  ply1coe  22303  evls1addd  22376  evls1muld  22377  evls1vsca  22378  rhmply1  22391  rhmply1vsca  22393  scmatscmiddistr  22515  1marepvsma1  22590  decpmatmulsumfsupp  22780  pmatcollpw1lem2  22782  pmatcollpwscmatlem1  22796  mptcoe1matfsupp  22809  mp2pm2mplem4  22816  chmatval  22836  chpidmat  22854  xpsdsval  24392  blres  24442  nmfval0  24604  nmval2  24606  ngpocelbl  24726  cncfmet  24936  ehl2eudisval  25458  minveclem2  25461  minveclem3b  25463  minveclem4  25467  minveclem6  25469  ply1divalg2  26179  clwwlknon1  30117  clwwlknon1nloop  30119  clwwlknon2  30122  nvm  30661  opprqusplusg  33518  zringfrac  33583  evls1subd  33598  algextdeglem8  33766  madjusmdetlem1  33827  xrge0pluscn  33940  esumpfinvallem  34076  ptrecube  37628  equivbnd2  37800  ismtyres  37816  iccbnd  37848  exidreslem  37885  iscrngo2  38005  toycom  38975  aks6d1c1p5  42114  aks5lem3a  42191  frlmsnic  42555  mendplusgfval  43198  sge0tsms  46400  vonn0ioo  46707  vonn0icc  46708  zlmodzxzadd  48279  snlindsntor  48393  isisod  48925  upeu2lem  48926  cofuswapf2  49013  indthinc  49134  indthincALT  49135  prsthinc  49136  mndtchom  49236