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

Theorem addass 9368
Description: Alias for ax-addass 9346, for naming consistency with addassi 9393. (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 9346 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 965    = wceq 1369    e. wcel 1756  (class class class)co 6090   CCcc 9279    + caddc 9284
This theorem was proved from axioms:  ax-addass 9346
This theorem is referenced by:  addassi  9393  addassd  9407  00id  9543  addid2  9551  add12  9581  add32  9582  add32r  9583  add4  9584  nnaddcl  10343  nneo  10724  uzaddcl  10910  xaddass  11211  fztp  11511  seradd  11847  expadd  11905  bernneq  11989  faclbnd6  12074  hashgadd  12139  swrds2  12544  clim2ser  13131  clim2ser2  13132  summolem3  13190  isumsplit  13302  odd2np1lem  13590  prmlem0  14132  cnaddablx  16347  cnaddabl  16348  zaddablx  16349  cncrng  17836  pjthlem1  20923  ptolemy  21957  bcp1ctr  22617  wlkdvspthlem  23505  gxnn0add  23760  cnaddablo  23836  pjhthlem1  24793  fsumcube  28202  mblfinlem2  28427  fzosplitpr  30221
  Copyright terms: Public domain W3C validator