Theorem addass 7941

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

Syntax hints:   -> wi 4   /\ w3a 978   = wceq 1353   e. wcel 2148  (class class class)co 5875   CCcc 7809   + caddc 7814

This theorem was proved from axioms:  ax-addass 7913

This theorem is referenced by:  addassi  7965  addassd  7980  add12  8115  add32  8116  add32r  8117  add4  8118  nnaddcl  8939  uzaddcl  9586  xaddass  9869  fztp  10078  ser3add  10505  expadd  10562  bernneq  10641  faclbnd6  10724  resqrexlemover  11019  clim2ser  11345  clim2ser2  11346  summodclem3  11388  isumsplit  11499  cvgratnnlemseq  11534  odd2np1lem  11877  cncrng  13466  ptolemy  14248