Theorem addass 8309

Description: Alias for ax-addass 8281, for naming consistency with addassi 8334. (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 8281	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 8177   + caddc 8182

This proof depends on axioms:  ax-addass 8281

This theorem is used by:  addassi  8334  addassd  8348  add12  8484  add32  8485  add32r  8486  add4  8487  nnaddcl  9324  uzaddcl  9986  xaddass  10271  fztp  10485  ser3add  10959  expadd  11018  bernneq  11098  faclbnd6  11182  resqrexlemover  11776  clim2ser  12103  clim2ser2  12104  summodclem3  12147  isumsplit  12258  cvgratnnlemseq  12293  odd2np1lem  12639  cncrng  14906  ptolemy  15925