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

Theorem oveqi 6818
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 6811 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624  (class class class)co 6805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808
This theorem is referenced by:  oveq123i  6819  cantnfval2  8731  vdwap1  15875  vdwlem12  15890  prdsdsval3  16339  oppchom  16568  rcaninv  16647  initoeu2lem0  16856  yonedalem21  17106  yonedalem22  17111  mndprop  17510  issubm  17540  frmdadd  17585  grpprop  17631  oppgplus  17971  ablprop  18396  ringpropd  18774  crngpropd  18775  ringprop  18776  opprmul  18818  opprringb  18824  mulgass3  18829  rngidpropd  18887  invrpropd  18890  drngprop  18952  subrgpropd  19008  rhmpropd  19009  lidlacl  19407  lidlmcl  19411  lidlrsppropd  19424  crngridl  19432  psradd  19576  ressmpladd  19651  ressmplmul  19652  ressmplvsca  19653  ressply1add  19794  ressply1mul  19795  ressply1vsca  19796  ply1coe  19860  scmatscmiddistr  20508  1marepvsma1  20583  decpmatmulsumfsupp  20772  pmatcollpw1lem2  20774  pmatcollpwscmatlem1  20788  mptcoe1matfsupp  20801  mp2pm2mplem4  20808  chmatval  20828  chpidmat  20846  xpsdsval  22379  blres  22429  nmfval2  22588  nmval2  22589  ngpocelbl  22701  cncfmet  22904  minveclem2  23389  minveclem3b  23391  minveclem4  23395  minveclem6  23397  ply1divalg2  24089  clwwlknonOLD  27228  clwwlknon1  27237  clwwlknon1nloop  27239  clwwlknon2  27242  nvm  27797  madjusmdetlem1  30194  xrge0pluscn  30287  esumpfinvallem  30437  ptrecube  33714  equivbnd2  33896  ismtyres  33912  iccbnd  33944  exidreslem  33981  iscrngo2  34101  toycom  34755  mendplusgfval  38249  sge0tsms  41092  vonn0ioo  41399  vonn0icc  41400  issubmgm  42291  rhmsubclem4  42591  zlmodzxzadd  42638  snlindsntor  42762
  Copyright terms: Public domain W3C validator