Theorem addass 10061

Description: Alias for ax-addass 10039, for naming consistency with addassi 10086. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
addass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addass

Step	Hyp	Ref	Expression
1		ax-addass 10039	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Syntax hints:   → wi 4   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  (class class class)co 6690  ℂcc 9972   + caddc 9977

This theorem was proved from axioms:  ax-addass 10039

This theorem is referenced by:  addassi  10086  addassd  10100  00id  10249  addid2  10257  add12  10291  add32  10292  add32r  10293  add4  10294  nnaddcl  11080  uzaddcl  11782  xaddass  12117  fztp  12435  seradd  12883  expadd  12942  bernneq  13030  faclbnd6  13126  hashgadd  13204  swrds2  13731  clim2ser  14429  clim2ser2  14430  summolem3  14489  isumsplit  14616  fsumcube  14835  odd2np1lem  15111  prmlem0  15859  cnaddablx  18317  cnaddabl  18318  zaddablx  18321  cncrng  19815  cnlmod  22986  pjthlem1  23254  ptolemy  24293  bcp1ctr  25049  cnaddabloOLD  27564  pjhthlem1  28378  dnibndlem5  32597  mblfinlem2  33577  mogoldbblem  41954  nnsgrp  42142  2zrngasgrp  42265