Theorem addass 8299

Description: Alias for ax-addass 8271, for naming consistency with addassi 8324. (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 8271	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )

Syntax hints:   -> wi 4   /\ w3a 1009   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   + caddc 8172

This theorem was proved from axioms:  ax-addass 8271

This theorem is referenced by:  addassi  8324  addassd  8338  add12  8474  add32  8475  add32r  8476  add4  8477  nnaddcl  9303  uzaddcl  9965  xaddass  10250  fztp  10463  ser3add  10937  expadd  10996  bernneq  11076  faclbnd6  11160  resqrexlemover  11754  clim2ser  12081  clim2ser2  12082  summodclem3  12125  isumsplit  12236  cvgratnnlemseq  12271  odd2np1lem  12617  cncrng  14878  ptolemy  15848