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

Theorem addass 9069
Description: Alias for ax-addass 9047, for naming consistency with addassi 9090. (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 9047 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 1652    e. wcel 1725  (class class class)co 6073   CCcc 8980    + caddc 8985
This theorem is referenced by:  addassi  9090  addassd  9102  00id  9233  addid2  9241  add12  9271  add32  9272  add4  9273  nnaddcl  10014  nneo  10345  uzaddcl  10525  xaddass  10820  fztp  11094  seradd  11357  expadd  11414  bernneq  11497  faclbnd6  11582  hashgadd  11643  swrds2  11872  clim2ser  12440  clim2ser2  12441  summolem3  12500  bcxmaslem2  12606  isumsplit  12612  odd2np1lem  12899  prmlem0  13420  cnaddablx  15473  cnaddabl  15474  zaddablx  15475  cncrng  16714  pjthlem1  19330  ptolemy  20396  bcp1ctr  21055  wlkdvspthlem  21599  gxnn0add  21854  cnaddablo  21930  pjhthlem1  22885  fsumcube  26098  mblfinlem  26234
This theorem was proved from axioms:  ax-addass 9047
  Copyright terms: Public domain W3C validator