Theorem addass 11125

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041

This theorem was proved from axioms:  ax-addass 11103

This theorem is referenced by:  addassi  11154  addassd  11166  00id  11320  addlid  11328  add12  11363  add32  11364  add32r  11365  add4  11366  nnaddcl  12180  uzaddcl  12829  xaddass  13176  fztp  13508  seradd  13979  expadd  14039  bernneq  14164  faclbnd6  14234  hashgadd  14312  swrds2  14875  clim2ser  15590  clim2ser2  15591  summolem3  15649  isumsplit  15775  fsumcube  15995  odd2np1lem  16279  prmlem0  17045  cnaddablx  19809  cnaddabl  19810  zaddablx  19813  cncrng  21355  cncrngOLD  21356  cnlmod  25108  pjthlem1  25405  ptolemy  26473  bcp1ctr  27258  cnaddabloOLD  30669  pjhthlem1  31479  dnibndlem5  36704  mblfinlem2  37909  facp2  42513  mogoldbblem  48080  nnsgrp  48537  nn0mnd  48539  2zrngasgrp  48606