Theorem addass 7011

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

Syntax hints:   -> wi 4   /\ w3a 885   = wceq 1243   e. wcel 1393  (class class class)co 5512   CCcc 6887   + caddc 6892

This theorem was proved from axioms:  ax-addass 6986

This theorem is referenced by:  addassi  7035  addassd  7049  add12  7169  add32  7170  add32r  7171  add4  7172  nnaddcl  7934  uzaddcl  8529  fztp  8940  iseradd  9243  expadd  9297  bernneq  9369  resqrexlemover  9608  clim2iser  9857  clim2iser2  9858