Theorem addass 8026

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

Syntax hints:   -> wi 4   /\ w3a 980   = wceq 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   + caddc 7899

This theorem was proved from axioms:  ax-addass 7998

This theorem is referenced by:  addassi  8051  addassd  8066  add12  8201  add32  8202  add32r  8203  add4  8204  nnaddcl  9027  uzaddcl  9677  xaddass  9961  fztp  10170  ser3add  10631  expadd  10690  bernneq  10769  faclbnd6  10853  resqrexlemover  11192  clim2ser  11519  clim2ser2  11520  summodclem3  11562  isumsplit  11673  cvgratnnlemseq  11708  odd2np1lem  12054  cncrng  14201  ptolemy  15144