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

Theorem addass 9033
Description: Alias for ax-addass 9011, for naming consistency with addassi 9054. (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 9011 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 1721  (class class class)co 6040   CCcc 8944    + caddc 8949
This theorem is referenced by:  addassi  9054  addassd  9066  00id  9197  addid2  9205  add12  9235  add32  9236  add4  9237  nnaddcl  9978  nneo  10309  uzaddcl  10489  xaddass  10784  fztp  11058  seradd  11320  expadd  11377  bernneq  11460  faclbnd6  11545  hashgadd  11606  swrds2  11835  clim2ser  12403  clim2ser2  12404  summolem3  12463  bcxmaslem2  12569  isumsplit  12575  odd2np1lem  12862  prmlem0  13383  cnaddablx  15436  cnaddabl  15437  zaddablx  15438  cncrng  16677  pjthlem1  19291  ptolemy  20357  bcp1ctr  21016  wlkdvspthlem  21560  gxnn0add  21815  cnaddablo  21891  pjhthlem1  22846  fsumcube  26010  mblfinlem  26143
This theorem was proved from axioms:  ax-addass 9011
  Copyright terms: Public domain W3C validator