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

Theorem oveqi 5955
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 5948 . 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 1642  (class class class)co 5942
This theorem is referenced by:  oveq123i  5956  cantnfval2  7457  vdwap1  13115  vdwlem12  13130  prdsdsval3  13477  oppchom  13711  yonedalem21  14140  yonedalem22  14145  mndprop  14493  issubm  14518  frmdadd  14570  grpprop  14594  oppgplus  14915  ablprop  15193  rngpropd  15465  crngpropd  15466  rngprop  15467  opprmul  15501  opprrngb  15507  mulgass3  15512  rngidpropd  15570  invrpropd  15573  drngprop  15616  subrgpropd  15672  rhmpropd  15673  lidlacl  16058  lidlmcl  16062  lidlrsppropd  16075  crngridl  16083  psradd  16220  ressmpladd  16294  ressmplmul  16295  ressmplvsca  16296  ressply1add  16401  ressply1mul  16402  ressply1vsca  16403  ply1coe  16461  xpsdsval  18041  blres  18073  nmfval2  18209  nmval2  18210  cncfmet  18509  minveclem2  18888  minveclem3b  18890  minveclem4  18894  minveclem6  18896  ply1divalg2  19622  issubgoi  21083  ghgrplem2  21140  nvm  21307  xrge0pluscn  23482  esumpfinvallem  23730  equivbnd2  25839  ismtyres  25855  iccbnd  25887  exidreslem  25890  iscrngo2  25946  mendplusgfval  26816  toycom  29214
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-uni 3907  df-br 4103  df-iota 5298  df-fv 5342  df-ov 5945
  Copyright terms: Public domain W3C validator