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

Theorem addass 9579
Description: Alias for ax-addass 9557, for naming consistency with addassi 9604. (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 9557 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973    = wceq 1379    e. wcel 1767  (class class class)co 6284   CCcc 9490    + caddc 9495
This theorem was proved from axioms:  ax-addass 9557
This theorem is referenced by:  addassi  9604  addassd  9618  00id  9754  addid2  9762  add12  9792  add32  9793  add32r  9794  add4  9795  nnaddcl  10558  nneo  10944  uzaddcl  11137  xaddass  11441  fztp  11736  seradd  12117  expadd  12176  bernneq  12260  faclbnd6  12345  hashgadd  12413  swrds2  12846  clim2ser  13440  clim2ser2  13441  summolem3  13499  isumsplit  13615  odd2np1lem  13904  prmlem0  14449  cnaddablx  16677  cnaddabl  16678  zaddablx  16679  cncrng  18238  pjthlem1  21615  ptolemy  22650  bcp1ctr  23310  wlkdvspthlem  24313  gxnn0add  24980  cnaddablo  25056  pjhthlem1  26013  fsumcube  29427  mblfinlem2  29657  fzosplitpr  31837
  Copyright terms: Public domain W3C validator