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

Theorem addass 9082
Description: Alias for ax-addass 9060, for naming consistency with addassi 9103. (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 9060 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 937    = wceq 1653    e. wcel 1726  (class class class)co 6084   CCcc 8993    + caddc 8998
This theorem is referenced by:  addassi  9103  addassd  9115  00id  9246  addid2  9254  add12  9284  add32  9285  add4  9286  nnaddcl  10027  nneo  10358  uzaddcl  10538  xaddass  10833  fztp  11107  seradd  11370  expadd  11427  bernneq  11510  faclbnd6  11595  hashgadd  11656  swrds2  11885  clim2ser  12453  clim2ser2  12454  summolem3  12513  bcxmaslem2  12619  isumsplit  12625  odd2np1lem  12912  prmlem0  13433  cnaddablx  15486  cnaddabl  15487  zaddablx  15488  cncrng  16727  pjthlem1  19343  ptolemy  20409  bcp1ctr  21068  wlkdvspthlem  21612  gxnn0add  21867  cnaddablo  21943  pjhthlem1  22898  fsumcube  26111  mblfinlem2  26255
This theorem was proved from axioms:  ax-addass 9060
  Copyright terms: Public domain W3C validator