Theorem addass 8090

Description: Alias for ax-addass 8062, for naming consistency with addassi 8115. (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 8062	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 2178  (class class class)co 5967   CCcc 7958   + caddc 7963

This theorem was proved from axioms:  ax-addass 8062

This theorem is referenced by:  addassi  8115  addassd  8130  add12  8265  add32  8266  add32r  8267  add4  8268  nnaddcl  9091  uzaddcl  9742  xaddass  10026  fztp  10235  ser3add  10704  expadd  10763  bernneq  10842  faclbnd6  10926  resqrexlemover  11436  clim2ser  11763  clim2ser2  11764  summodclem3  11806  isumsplit  11917  cvgratnnlemseq  11952  odd2np1lem  12298  cncrng  14446  ptolemy  15411