Theorem addass 8309

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182

This proof depends on axioms:  ax-addass 8281

This theorem is used by:  addassi  8334  addassd  8348  add12  8485  add32  8486  add32r  8487  add4  8488  nnaddcl  9326  uzaddcl  9995  xaddass  10281  fztp  10495  ser3add  10972  expadd  11031  bernneq  11111  faclbnd6  11196  resqrexlemover  11790  clim2ser  12119  clim2ser2  12120  summodclem3  12163  isumsplit  12274  cvgratnnlemseq  12309  odd2np1lem  12655  prmlem0  13240  cncrng  14955  ptolemy  15975  bcp1ctr  16204