Theorem addass 11211

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

Assertion

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

Proof of Theorem addass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122   + caddc 11127

This proof depends on axioms:  ax-addass 11189

This theorem is used by:  addassi  11243  addassd  11255  00id  11409  addlid  11417  add12  11452  add32  11453  add32r  11454  add4  11455  nnaddcl  12280  uzaddcl  12953  xaddass  13301  fztp  13635  seradd  14108  expadd  14168  bernneq  14293  faclbnd6  14363  hashgadd  14441  swrds2  15011  clim2ser  15742  clim2ser2  15743  summolem3  15800  isumsplit  15929  fsumcube  16146  odd2np1lem  16430  prmlem0  17197  cnaddablx  19995  cnaddabl  19996  zaddablx  19999  cncrng  21606  cnlmod  25368  pjthlem1  25665  ptolemy  26734  bcp1ctr  27515  cnaddabloOLD  31062  pjhthlem1  31872  dnibndlem5  37179  mblfinlem2  38407  facp2  43009  mogoldbblem  48636  nnsgrp  49092  nn0mnd  49094  2zrngasgrp  49161