Theorem addass 7862

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

Syntax hints:   -> wi 4   /\ w3a 963   = wceq 1335   e. wcel 2128  (class class class)co 5824   CCcc 7730   + caddc 7735

This theorem was proved from axioms:  ax-addass 7834

This theorem is referenced by:  addassi  7886  addassd  7900  add12  8033  add32  8034  add32r  8035  add4  8036  nnaddcl  8853  uzaddcl  9497  xaddass  9773  fztp  9980  ser3add  10404  expadd  10461  bernneq  10538  faclbnd6  10618  resqrexlemover  10910  clim2ser  11234  clim2ser2  11235  summodclem3  11277  isumsplit  11388  cvgratnnlemseq  11423  odd2np1lem  11763  ptolemy  13156