Theorem addass 8057

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

Syntax hints:   -> wi 4   /\ w3a 981   = wceq 1373   e. wcel 2176  (class class class)co 5946   CCcc 7925   + caddc 7930

This theorem was proved from axioms:  ax-addass 8029

This theorem is referenced by:  addassi  8082  addassd  8097  add12  8232  add32  8233  add32r  8234  add4  8235  nnaddcl  9058  uzaddcl  9709  xaddass  9993  fztp  10202  ser3add  10669  expadd  10728  bernneq  10807  faclbnd6  10891  resqrexlemover  11354  clim2ser  11681  clim2ser2  11682  summodclem3  11724  isumsplit  11835  cvgratnnlemseq  11870  odd2np1lem  12216  cncrng  14364  ptolemy  15329