Theorem addass 8257

Description: Alias for ax-addass 8229, for naming consistency with addassi 8282. (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

Step	Hyp	Ref	Expression
1		ax-addass 8229	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )

Syntax hints:   -> wi 4   /\ w3a 1005   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   + caddc 8130

This theorem was proved from axioms:  ax-addass 8229

This theorem is referenced by:  addassi  8282  addassd  8296  add12  8431  add32  8432  add32r  8433  add4  8434  nnaddcl  9257  uzaddcl  9918  xaddass  10202  fztp  10412  ser3add  10884  expadd  10943  bernneq  11022  faclbnd6  11106  resqrexlemover  11695  clim2ser  12022  clim2ser2  12023  summodclem3  12066  isumsplit  12177  cvgratnnlemseq  12212  odd2np1lem  12558  cncrng  14717  ptolemy  15689