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

Theorem oveqi 5871
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 5864 . 2  |-  ( A  =  B  ->  ( C A D )  =  ( C B D ) )
31, 2ax-mp 8 1  |-  ( C A D )  =  ( C B D )
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858
This theorem is referenced by:  oveq123i  5872  cantnfval2  7370  vdwap1  13024  vdwlem12  13039  prdsdsval3  13384  oppchom  13618  yonedalem21  14047  yonedalem22  14052  mndprop  14400  issubm  14425  frmdadd  14477  grpprop  14501  oppgplus  14822  ablprop  15100  rngpropd  15372  crngpropd  15373  rngprop  15374  opprmul  15408  opprrngb  15414  mulgass3  15419  rngidpropd  15477  invrpropd  15480  drngprop  15523  subrgpropd  15579  rhmpropd  15580  lidlacl  15965  lidlmcl  15969  lidlrsppropd  15982  crngridl  15990  psradd  16127  ressmpladd  16201  ressmplmul  16202  ressmplvsca  16203  ressply1add  16308  ressply1mul  16309  ressply1vsca  16310  ply1coe  16368  xpsdsval  17945  blres  17977  nmfval2  18113  nmval2  18114  cncfmet  18412  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  ply1divalg2  19524  issubgoi  20977  ghgrplem2  21034  nvm  21199  xrge0pluscn  23322  esumpfinvallem  23442  vecval3b  25452  cnegvex2b  25662  rnegvex2b  25663  addcanrg  25667  isder  25707  equivbnd2  26516  ismtyres  26532  iccbnd  26564  exidreslem  26567  iscrngo2  26623  mendplusgfval  27493  toycom  29162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator