Theorem addass 8055

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

Syntax hints:   -> wi 4   /\ w3a 981   = wceq 1373   e. wcel 2176  (class class class)co 5944   CCcc 7923   + caddc 7928

This theorem was proved from axioms:  ax-addass 8027

This theorem is referenced by:  addassi  8080  addassd  8095  add12  8230  add32  8231  add32r  8232  add4  8233  nnaddcl  9056  uzaddcl  9707  xaddass  9991  fztp  10200  ser3add  10667  expadd  10726  bernneq  10805  faclbnd6  10889  resqrexlemover  11321  clim2ser  11648  clim2ser2  11649  summodclem3  11691  isumsplit  11802  cvgratnnlemseq  11837  odd2np1lem  12183  cncrng  14331  ptolemy  15296