Theorem addass 7904

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

Syntax hints:   -> wi 4   /\ w3a 973   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   + caddc 7777

This theorem was proved from axioms:  ax-addass 7876

This theorem is referenced by:  addassi  7928  addassd  7942  add12  8077  add32  8078  add32r  8079  add4  8080  nnaddcl  8898  uzaddcl  9545  xaddass  9826  fztp  10034  ser3add  10461  expadd  10518  bernneq  10596  faclbnd6  10678  resqrexlemover  10974  clim2ser  11300  clim2ser2  11301  summodclem3  11343  isumsplit  11454  cvgratnnlemseq  11489  odd2np1lem  11831  ptolemy  13539