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

Theorem oveqi 7164
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 7157 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-rex 3148  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-ov 7154
This theorem is referenced by:  oveq123i  7165  cantnfval2  9124  vdwap1  16305  vdwlem12  16320  prdsdsval3  16750  oppchom  16977  rcaninv  17056  initoeu2lem0  17265  yonedalem21  17515  yonedalem22  17520  mndprop  17927  issubm  17958  frmdadd  18005  grpprop  18051  oppgplus  18409  ablprop  18840  ringpropd  19254  crngpropd  19255  ringprop  19256  opprmul  19298  opprringb  19304  mulgass3  19309  rngidpropd  19367  invrpropd  19370  drngprop  19435  subrgpropd  19492  rhmpropd  19493  lidlacl  19907  lidlmcl  19911  lidlrsppropd  19924  crngridl  19932  psradd  20083  ressmpladd  20158  ressmplmul  20159  ressmplvsca  20160  ressply1add  20315  ressply1mul  20316  ressply1vsca  20317  ply1coe  20381  scmatscmiddistr  21033  1marepvsma1  21108  decpmatmulsumfsupp  21297  pmatcollpw1lem2  21299  pmatcollpwscmatlem1  21313  mptcoe1matfsupp  21326  mp2pm2mplem4  21333  chmatval  21353  chpidmat  21371  xpsdsval  22906  blres  22956  nmfval2  23115  nmval2  23116  ngpocelbl  23228  cncfmet  23431  ehl2eudisval  23941  minveclem2  23944  minveclem3b  23946  minveclem4  23950  minveclem6  23952  ply1divalg2  24647  clwwlknon1  27791  clwwlknon1nloop  27793  clwwlknon2  27796  nvm  28333  madjusmdetlem1  30979  xrge0pluscn  31070  esumpfinvallem  31220  ptrecube  34760  equivbnd2  34939  ismtyres  34955  iccbnd  34987  exidreslem  35024  iscrngo2  35144  toycom  35977  frlmsnic  39013  mendplusgfval  39647  sge0tsms  42525  vonn0ioo  42832  vonn0icc  42833  issubmgm  43885  rhmsubclem4  44189  zlmodzxzadd  44235  snlindsntor  44355
  Copyright terms: Public domain W3C validator