Theorem addass 8140

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

Syntax hints:   -> wi 4   /\ w3a 1002   = wceq 1395   e. wcel 2200  (class class class)co 6007   CCcc 8008   + caddc 8013

This theorem was proved from axioms:  ax-addass 8112

This theorem is referenced by:  addassi  8165  addassd  8180  add12  8315  add32  8316  add32r  8317  add4  8318  nnaddcl  9141  uzaddcl  9793  xaddass  10077  fztp  10286  ser3add  10756  expadd  10815  bernneq  10894  faclbnd6  10978  resqrexlemover  11537  clim2ser  11864  clim2ser2  11865  summodclem3  11907  isumsplit  12018  cvgratnnlemseq  12053  odd2np1lem  12399  cncrng  14549  ptolemy  15514