Theorem addass 7103

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

Syntax hints:   -> wi 4   /\ w3a 919   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   + caddc 6984

This theorem was proved from axioms:  ax-addass 7078

This theorem is referenced by:  addassi  7127  addassd  7141  add12  7266  add32  7267  add32r  7268  add4  7269  nnaddcl  8059  uzaddcl  8674  fztp  9095  iseradd  9463  expadd  9518  bernneq  9593  faclbnd6  9671  resqrexlemover  9896  clim2iser  10175  clim2iser2  10176  odd2np1lem  10271