Theorem addass 7940

Description: Alias for ax-addass 7912, for naming consistency with addassi 7964. (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 7912	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 5874   CCcc 7808   + caddc 7813

This theorem was proved from axioms:  ax-addass 7912

This theorem is referenced by:  addassi  7964  addassd  7979  add12  8114  add32  8115  add32r  8116  add4  8117  nnaddcl  8938  uzaddcl  9585  xaddass  9868  fztp  10077  ser3add  10504  expadd  10561  bernneq  10640  faclbnd6  10723  resqrexlemover  11018  clim2ser  11344  clim2ser2  11345  summodclem3  11387  isumsplit  11498  cvgratnnlemseq  11533  odd2np1lem  11876  cncrng  13433  ptolemy  14215