Theorem addass 8310

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   + caddc 8183

This proof depends on axioms:  ax-addass 8282

This theorem is used by:  addassi  8335  addassd  8349  add12  8486  add32  8487  add32r  8488  add4  8489  nnaddcl  9327  uzaddcl  9996  xaddass  10282  fztp  10496  ser3add  10974  expadd  11033  bernneq  11113  faclbnd6  11198  resqrexlemover  11792  clim2ser  12122  clim2ser2  12123  summodclem3  12166  isumsplit  12277  cvgratnnlemseq  12312  odd2np1lem  12658  prmlem0  13243  cncrng  14990  ptolemy  16017  bcp1ctr  16267