Theorem addass 7938

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

Syntax hints:   -> wi 4   /\ w3a 978   = wceq 1353   e. wcel 2148  (class class class)co 5872   CCcc 7806   + caddc 7811

This theorem was proved from axioms:  ax-addass 7910

This theorem is referenced by:  addassi  7962  addassd  7976  add12  8111  add32  8112  add32r  8113  add4  8114  nnaddcl  8935  uzaddcl  9582  xaddass  9865  fztp  10073  ser3add  10500  expadd  10557  bernneq  10635  faclbnd6  10717  resqrexlemover  11012  clim2ser  11338  clim2ser2  11339  summodclem3  11381  isumsplit  11492  cvgratnnlemseq  11527  odd2np1lem  11869  cncrng  13332  ptolemy  14116