Theorem addass 11292

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

Assertion

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

Proof of Theorem addass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  (class class class)co 7422  ℂcc 11203   + caddc 11208

This proof depends on axioms:  ax-addass 11270

This theorem is used by:  addassi  11324  addassd  11336  00id  11490  addlid  11498  add12  11533  add32  11534  add32r  11535  add4  11536  nnaddcl  12363  uzaddcl  13036  xaddass  13384  fztp  13719  seradd  14192  expadd  14252  bernneq  14378  faclbnd6  14448  hashgadd  14526  swrds2  15098  clim2ser  15829  clim2ser2  15830  summolem3  15887  isumsplit  16016  fsumcube  16233  odd2np1lem  16517  prmlem0  17290  cnaddablx  20089  cnaddabl  20090  zaddablx  20093  cncrng  21706  cnlmod  25468  pjthlem1  25765  ptolemy  26832  bcp1ctr  27613  cnaddabloOLD  31190  pjhthlem1  32000  dnibndlem5  37442  mblfinlem2  38683  facp2  43300  mogoldbblem  48925  nnsgrp  49381  nn0mnd  49383  2zrngasgrp  49450