Theorem addass 7472

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

Syntax hints:   -> wi 4   /\ w3a 924   = wceq 1289   e. wcel 1438  (class class class)co 5652   CCcc 7348   + caddc 7353

This theorem was proved from axioms:  ax-addass 7447

This theorem is referenced by:  addassi  7496  addassd  7510  add12  7640  add32  7641  add32r  7642  add4  7643  nnaddcl  8442  uzaddcl  9074  fztp  9492  iseradd  9934  expadd  9997  bernneq  10074  faclbnd6  10152  resqrexlemover  10443  clim2ser  10725  clim2ser2  10726  isummolem3  10770  isumsplit  10885  cvgratnnlemseq  10920  odd2np1lem  11150