Theorem addass 8315

Description: Alias for ax-addass 8287, for naming consistency with addassi 8340. (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 8287	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 6088   CCcc 8183   + caddc 8188

This proof depends on axioms:  ax-addass 8287

This theorem is used by:  addassi  8340  addassd  8354  add12  8491  add32  8492  add32r  8493  add4  8494  nnaddcl  9333  uzaddcl  10002  xaddass  10288  fztp  10502  ser3add  10980  expadd  11039  bernneq  11119  faclbnd6  11204  resqrexlemover  11798  clim2ser  12128  clim2ser2  12129  summodclem3  12172  isumsplit  12283  cvgratnnlemseq  12318  odd2np1lem  12664  prmlem0  13249  cncrng  15015  ptolemy  16051  bcp1ctr  16306