Theorem addass 7883

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

Syntax hints:   -> wi 4   /\ w3a 968   = wceq 1343   e. wcel 2136  (class class class)co 5842   CCcc 7751   + caddc 7756

This theorem was proved from axioms:  ax-addass 7855

This theorem is referenced by:  addassi  7907  addassd  7921  add12  8056  add32  8057  add32r  8058  add4  8059  nnaddcl  8877  uzaddcl  9524  xaddass  9805  fztp  10013  ser3add  10440  expadd  10497  bernneq  10575  faclbnd6  10657  resqrexlemover  10952  clim2ser  11278  clim2ser2  11279  summodclem3  11321  isumsplit  11432  cvgratnnlemseq  11467  odd2np1lem  11809  ptolemy  13385