Theorem addass 8273

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

Syntax hints:   -> wi 4   /\ w3a 1005   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   + caddc 8146

This theorem was proved from axioms:  ax-addass 8245

This theorem is referenced by:  addassi  8298  addassd  8312  add12  8447  add32  8448  add32r  8449  add4  8450  nnaddcl  9274  uzaddcl  9936  xaddass  10221  fztp  10434  ser3add  10908  expadd  10967  bernneq  11047  faclbnd6  11131  resqrexlemover  11720  clim2ser  12047  clim2ser2  12048  summodclem3  12091  isumsplit  12202  cvgratnnlemseq  12237  odd2np1lem  12583  cncrng  14843  ptolemy  15815