Theorem addass 11280

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

Assertion

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

Proof of Theorem addass

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

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

This proof depends on axioms:  ax-addass 11258

This theorem is used by:  addassi  11312  addassd  11324  00id  11478  addlid  11486  add12  11521  add32  11522  add32r  11523  add4  11524  nnaddcl  12351  uzaddcl  13024  xaddass  13372  fztp  13707  seradd  14180  expadd  14240  bernneq  14366  faclbnd6  14436  hashgadd  14514  swrds2  15084  clim2ser  15815  clim2ser2  15816  summolem3  15873  isumsplit  16002  fsumcube  16219  odd2np1lem  16503  prmlem0  17276  cnaddablx  20075  cnaddabl  20076  zaddablx  20079  cncrng  21692  cnlmod  25454  pjthlem1  25751  ptolemy  26818  bcp1ctr  27599  cnaddabloOLD  31176  pjhthlem1  31986  dnibndlem5  37328  mblfinlem2  38556  facp2  43173  mogoldbblem  48787  nnsgrp  49243  nn0mnd  49245  2zrngasgrp  49312