Theorem addass 8129

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

Syntax hints:   -> wi 4   /\ w3a 1002   = wceq 1395   e. wcel 2200  (class class class)co 6001   CCcc 7997   + caddc 8002

This theorem was proved from axioms:  ax-addass 8101

This theorem is referenced by:  addassi  8154  addassd  8169  add12  8304  add32  8305  add32r  8306  add4  8307  nnaddcl  9130  uzaddcl  9781  xaddass  10065  fztp  10274  ser3add  10744  expadd  10803  bernneq  10882  faclbnd6  10966  resqrexlemover  11521  clim2ser  11848  clim2ser2  11849  summodclem3  11891  isumsplit  12002  cvgratnnlemseq  12037  odd2np1lem  12383  cncrng  14533  ptolemy  15498