Theorem oveqi 7372

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

Syntax hints:   = wceq 1548  (class class class)co 7359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3901  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362

This theorem is referenced by:  oveq123i  7373  fvmpopr2d  7521  cantnfval2  9585  vdwap1  16943  vdwlem12  16958  prdsdsval3  17443  oppchom  17676  rcaninv  17756  initoeu2lem0  17975  yonedalem21  18234  yonedalem22  18239  issubmgm  18665  mndprop  18723  issubm  18766  frmdadd  18818  smndex1sgrp  18874  smndex1mnd  18876  grpprop  18923  oppgplus  19318  ablprop  19762  ringpropd  20263  crngpropd  20264  ringprop  20265  opprmul  20314  opprrngb  20320  opprringb  20322  mulgass3  20327  rngidpropd  20389  invrpropd  20392  rhmimasubrng  20541  cntzsubrng  20542  subrngpropd  20543  subrgpropd  20583  rhmpropd  20584  rhmsubclem4  20663  drngprop  20719  lidlacl  21217  lidlrsppropd  21240  crngridl  21276  pzriprnglem5  21463  pzriprnglem6  21464  pzriprng1ALT  21474  psradd  21916  ressmpladd  22007  ressmplmul  22008  ressmplvsca  22009  ressply1add  22217  ressply1mul  22218  ressply1vsca  22219  ply1coe  22287  evls1addd  22360  evls1muld  22361  evls1vsca  22362  rhmply1  22372  rhmply1vsca  22374  scmatscmiddistr  22494  1marepvsma1  22569  decpmatmulsumfsupp  22759  pmatcollpw1lem2  22761  pmatcollpwscmatlem1  22775  mptcoe1matfsupp  22788  mp2pm2mplem4  22795  chmatval  22815  chpidmat  22833  xpsdsval  24367  blres  24417  nmfval0  24576  nmval2  24578  ngpocelbl  24690  cncfmet  24897  ehl2eudisval  25411  minveclem2  25414  minveclem3b  25416  minveclem4  25420  minveclem6  25422  ply1divalg2  26125  clwwlknon1  30187  clwwlknon1nloop  30189  clwwlknon2  30192  nvm  30732  opprqusplusg  33574  zringfrac  33647  evls1subd  33665  algextdeglem8  33918  madjusmdetlem1  34021  xrge0pluscn  34134  esumpfinvallem  34268  ptrecube  38000  equivbnd2  38172  ismtyres  38188  iccbnd  38220  exidreslem  38257  iscrngo2  38377  toycom  39478  aks6d1c1p5  42610  aks5lem3a  42687  frlmsnic  43039  mendplusgfval  43639  sge0tsms  46835  vonn0ioo  47142  vonn0icc  47143  zlmodzxzadd  48861  snlindsntor  48974  ovsng2  49361  isisod  49529  upeu2lem  49530  imaidfu  49612  cofuswapf2  49797  indthinc  49964  indthincALT  49965  prsthinc  49966  lmddu  50169