Theorem addass 11202

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

Assertion

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

Proof of Theorem addass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113   + caddc 11118

This proof depends on axioms:  ax-addass 11180

This theorem is used by:  addassi  11234  addassd  11246  00id  11400  addlid  11408  add12  11443  add32  11444  add32r  11445  add4  11446  nnaddcl  12271  uzaddcl  12944  xaddass  13291  fztp  13625  seradd  14098  expadd  14158  bernneq  14283  faclbnd6  14353  hashgadd  14431  swrds2  15001  clim2ser  15730  clim2ser2  15731  summolem3  15788  isumsplit  15917  fsumcube  16136  odd2np1lem  16420  prmlem0  17187  cnaddablx  19982  cnaddabl  19983  zaddablx  19986  cncrng  21593  cnlmod  25350  pjthlem1  25647  ptolemy  26712  bcp1ctr  27494  cnaddabloOLD  31004  pjhthlem1  31814  dnibndlem5  37128  mblfinlem2  38366  facp2  42968  mogoldbblem  48543  nnsgrp  48999  nn0mnd  49001  2zrngasgrp  49068