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

Theorem addass 9010
Description: Alias for ax-addass 8988, for naming consistency with addassi 9031. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addass  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 8988 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1717  (class class class)co 6020   CCcc 8921    + caddc 8926
This theorem is referenced by:  addassi  9031  addassd  9043  00id  9173  addid2  9181  add12  9211  add32  9212  add4  9213  nnaddcl  9954  nneo  10285  uzaddcl  10465  xaddass  10760  fztp  11034  seradd  11292  expadd  11349  bernneq  11432  faclbnd6  11517  hashgadd  11578  swrds2  11807  clim2ser  12375  clim2ser2  12376  summolem3  12435  bcxmaslem2  12541  isumsplit  12547  odd2np1lem  12834  prmlem0  13355  cnaddablx  15408  cnaddabl  15409  zaddablx  15410  cncrng  16645  pjthlem1  19205  ptolemy  20271  bcp1ctr  20930  wlkdvspthlem  21455  gxnn0add  21710  cnaddablo  21786  pjhthlem1  22741  fsumcube  25820
This theorem was proved from axioms:  ax-addass 8988
  Copyright terms: Public domain W3C validator