MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addass Structured version   Visualization version   GIF version

Theorem addass 10280
Description: Alias for ax-addass 10258, for naming consistency with addassi 10308. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 10258 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107   = wceq 1652  wcel 2155  (class class class)co 6846  cc 10191   + caddc 10196
This theorem was proved from axioms:  ax-addass 10258
This theorem is referenced by:  addassi  10308  addassd  10320  00id  10470  addid2  10478  add12  10512  add32  10513  add32r  10514  add4  10515  nnaddcl  11303  uzaddcl  11951  xaddass  12288  fztp  12611  seradd  13057  expadd  13116  bernneq  13204  faclbnd6  13297  hashgadd  13375  swrds2  13985  clim2ser  14686  clim2ser2  14687  summolem3  14746  isumsplit  14872  fsumcube  15089  odd2np1lem  15362  prmlem0  16102  cnaddablx  18553  cnaddabl  18554  zaddablx  18557  cncrng  20056  cnlmod  23234  pjthlem1  23513  ptolemy  24556  bcp1ctr  25311  cnaddabloOLD  27915  pjhthlem1  28729  dnibndlem5  32934  mblfinlem2  33894  mogoldbblem  42331  nnsgrp  42512  2zrngasgrp  42635
  Copyright terms: Public domain W3C validator