Theorem addass 10023

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

Syntax hints:   -> wi 4   /\ w3a 1037   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939

This theorem was proved from axioms:  ax-addass 10001

This theorem is referenced by:  addassi  10048  addassd  10062  00id  10211  addid2  10219  add12  10253  add32  10254  add32r  10255  add4  10256  nnaddcl  11042  uzaddcl  11744  xaddass  12079  fztp  12397  seradd  12843  expadd  12902  bernneq  12990  faclbnd6  13086  hashgadd  13166  swrds2  13685  clim2ser  14385  clim2ser2  14386  summolem3  14445  isumsplit  14572  fsumcube  14791  odd2np1lem  15064  prmlem0  15812  cnaddablx  18271  cnaddabl  18272  zaddablx  18275  cncrng  19767  cnlmod  22940  pjthlem1  23208  ptolemy  24248  bcp1ctr  25004  cnaddabloOLD  27436  pjhthlem1  28250  dnibndlem5  32472  mblfinlem2  33447  mogoldbblem  41629  nnsgrp  41817  2zrngasgrp  41940