MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveqi Structured version   Visualization version   GIF version

Theorem oveqi 7158
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
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq 7151 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rex 3141  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  oveq123i  7159  cantnfval2  9120  vdwap1  16301  vdwlem12  16316  prdsdsval3  16746  oppchom  16973  rcaninv  17052  initoeu2lem0  17261  yonedalem21  17511  yonedalem22  17516  mndprop  17925  issubm  17956  frmdadd  18008  grpprop  18057  oppgplus  18415  ablprop  18847  ringpropd  19261  crngpropd  19262  ringprop  19263  opprmul  19305  opprringb  19311  mulgass3  19316  rngidpropd  19374  invrpropd  19377  drngprop  19442  subrgpropd  19499  rhmpropd  19500  lidlacl  19914  lidlmcl  19918  lidlrsppropd  19931  crngridl  19939  psradd  20090  ressmpladd  20166  ressmplmul  20167  ressmplvsca  20168  ressply1add  20326  ressply1mul  20327  ressply1vsca  20328  ply1coe  20392  scmatscmiddistr  21045  1marepvsma1  21120  decpmatmulsumfsupp  21309  pmatcollpw1lem2  21311  pmatcollpwscmatlem1  21325  mptcoe1matfsupp  21338  mp2pm2mplem4  21345  chmatval  21365  chpidmat  21383  xpsdsval  22918  blres  22968  nmfval2  23127  nmval2  23128  ngpocelbl  23240  cncfmet  23443  ehl2eudisval  23953  minveclem2  23956  minveclem3b  23958  minveclem4  23962  minveclem6  23964  ply1divalg2  24659  clwwlknon1  27803  clwwlknon1nloop  27805  clwwlknon2  27808  nvm  28345  madjusmdetlem1  30991  xrge0pluscn  31082  esumpfinvallem  31232  ptrecube  34773  equivbnd2  34951  ismtyres  34967  iccbnd  34999  exidreslem  35036  iscrngo2  35156  toycom  35989  frlmsnic  39027  mendplusgfval  39663  sge0tsms  42539  vonn0ioo  42846  vonn0icc  42847  issubmgm  43933  smndex1sgrp  44008  smndex1mnd  44010  rhmsubclem4  44288  zlmodzxzadd  44334  snlindsntor  44454
  Copyright terms: Public domain W3C validator