Theorem addass 7753

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

Syntax hints:   -> wi 4   /\ w3a 962   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7621   + caddc 7626

This theorem was proved from axioms:  ax-addass 7725

This theorem is referenced by:  addassi  7777  addassd  7791  add12  7923  add32  7924  add32r  7925  add4  7926  nnaddcl  8743  uzaddcl  9384  xaddass  9655  fztp  9861  ser3add  10281  expadd  10338  bernneq  10415  faclbnd6  10493  resqrexlemover  10785  clim2ser  11109  clim2ser2  11110  summodclem3  11152  isumsplit  11263  cvgratnnlemseq  11298  odd2np1lem  11572  ptolemy  12908