Theorem addass 8222

Description: Alias for ax-addass 8194, for naming consistency with addassi 8247. (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 8194	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 2202  (class class class)co 6028   CCcc 8090   + caddc 8095

This theorem was proved from axioms:  ax-addass 8194

This theorem is referenced by:  addassi  8247  addassd  8261  add12  8396  add32  8397  add32r  8398  add4  8399  nnaddcl  9222  uzaddcl  9881  xaddass  10165  fztp  10375  ser3add  10847  expadd  10906  bernneq  10985  faclbnd6  11069  resqrexlemover  11650  clim2ser  11977  clim2ser2  11978  summodclem3  12021  isumsplit  12132  cvgratnnlemseq  12167  odd2np1lem  12513  cncrng  14665  ptolemy  15635