Theorem addass 7774

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

Syntax hints:   -> wi 4   /\ w3a 963   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   + caddc 7647

This theorem was proved from axioms:  ax-addass 7746

This theorem is referenced by:  addassi  7798  addassd  7812  add12  7944  add32  7945  add32r  7946  add4  7947  nnaddcl  8764  uzaddcl  9408  xaddass  9682  fztp  9889  ser3add  10309  expadd  10366  bernneq  10443  faclbnd6  10522  resqrexlemover  10814  clim2ser  11138  clim2ser2  11139  summodclem3  11181  isumsplit  11292  cvgratnnlemseq  11327  odd2np1lem  11605  ptolemy  12953