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

Theorem addass 8824
Description: Alias for ax-addass 8802, for naming consistency with addassi 8845. (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 8802 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 934    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740
This theorem is referenced by:  addassi  8845  addassd  8857  00id  8987  addid2  8995  add12  9025  add32  9026  add4  9027  nnaddcl  9768  nneo  10095  uzaddcl  10275  xaddass  10569  fztp  10841  seradd  11088  expadd  11144  bernneq  11227  faclbnd6  11312  hashgadd  11359  swrds2  11560  clim2ser  12128  clim2ser2  12129  summolem3  12187  bcxmaslem2  12293  isumsplit  12299  odd2np1lem  12586  prmlem0  13107  cnaddablx  15158  cnaddabl  15159  zaddablx  15160  cncrng  16395  pjthlem1  18801  ptolemy  19864  bcp1ctr  20518  gxnn0add  20941  cnaddablo  21017  pjhthlem1  21970  fsumcube  24795  mslb1  25607  2wsms  25608  stoweidlem13  27762
This theorem was proved from axioms:  ax-addass 8802
  Copyright terms: Public domain W3C validator