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

Theorem oveqi 6206
Description: Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
oveq1i.1  |-  A  =  B
Assertion
Ref Expression
oveqi  |-  ( C A D )  =  ( C B D )

Proof of Theorem oveqi
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq 6199 . 2  |-  ( A  =  B  ->  ( C A D )  =  ( C B D ) )
31, 2ax-mp 5 1  |-  ( C A D )  =  ( C B D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370  (class class class)co 6193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-uni 4193  df-br 4394  df-iota 5482  df-fv 5527  df-ov 6196
This theorem is referenced by:  oveq123i  6207  cantnfval2  7981  cantnfval2OLD  8011  vdwap1  14149  vdwlem12  14164  prdsdsval3  14534  oppchom  14765  yonedalem21  15194  yonedalem22  15199  mndprop  15559  issubm  15586  frmdadd  15644  grpprop  15668  oppgplus  15975  ablprop  16401  rngpropd  16791  crngpropd  16792  rngprop  16793  opprmul  16833  opprrngb  16839  mulgass3  16844  rngidpropd  16902  invrpropd  16905  drngprop  16958  subrgpropd  17014  rhmpropd  17015  lidlacl  17410  lidlmcl  17414  lidlrsppropd  17427  crngridl  17435  psradd  17568  ressmpladd  17652  ressmplmul  17653  ressmplvsca  17654  ressply1add  17800  ressply1mul  17801  ressply1vsca  17802  ply1coe  17864  ply1coeOLD  17865  1marepvsma1  18514  xpsdsval  20081  blres  20131  nmfval2  20308  nmval2  20309  cncfmet  20609  minveclem2  21038  minveclem3b  21040  minveclem4  21044  minveclem6  21046  ply1divalg2  21736  issubgoi  23942  ghgrplem2  23999  nvm  24166  xrge0pluscn  26508  esumpfinvallem  26661  equivbnd2  28832  ismtyres  28848  iccbnd  28880  exidreslem  28883  iscrngo2  28939  mendplusgfval  29683  zlmodzxzadd  30896  snlindsntor  31115  pmatcollpw1lem5  31234  pmatcollpwscmatlem1  31248  mptcoe1matfsupp  31252  mp2pm2mplem4  31267  cpidmat  31304  toycom  32927
  Copyright terms: Public domain W3C validator