Theorem addass 8162

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

Syntax hints:   -> wi 4   /\ w3a 1004   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

This theorem was proved from axioms:  ax-addass 8134

This theorem is referenced by:  addassi  8187  addassd  8202  add12  8337  add32  8338  add32r  8339  add4  8340  nnaddcl  9163  uzaddcl  9820  xaddass  10104  fztp  10313  ser3add  10785  expadd  10844  bernneq  10923  faclbnd6  11007  resqrexlemover  11588  clim2ser  11915  clim2ser2  11916  summodclem3  11959  isumsplit  12070  cvgratnnlemseq  12105  odd2np1lem  12451  cncrng  14602  ptolemy  15567