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 972    = wceq 1381    e. wcel 1802  (class class class)co 6278   CCcc 9490    + caddc 9495
This theorem was proved from axioms:  ax-addass 9557
This theorem is referenced by:  addassi  9604  addassd  9618  00id  9755  addid2  9763  add12  9793  add32  9794  add32r  9795  add4  9796  nnaddcl  10561  uzaddcl  11143  xaddass  11447  fztp  11742  seradd  12125  expadd  12184  bernneq  12268  faclbnd6  12353  hashgadd  12421  swrds2  12859  clim2ser  13453  clim2ser2  13454  summolem3  13512  isumsplit  13628  odd2np1lem  13919  prmlem0  14465  cnaddablx  16745  cnaddabl  16746  zaddablx  16747  cncrng  18310  pjthlem1  21722  ptolemy  22758  bcp1ctr  23423  wlkdvspthlem  24478  gxnn0add  25145  cnaddablo  25221  pjhthlem1  26178  fsumcube  29794  mblfinlem2  30024  nnsgrp  32342  2zrngasgrp  32453
  Copyright terms: Public domain W3C validator