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

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

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 10039 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972   + caddc 9977
This theorem was proved from axioms:  ax-addass 10039
This theorem is referenced by:  addassi  10086  addassd  10100  00id  10249  addid2  10257  add12  10291  add32  10292  add32r  10293  add4  10294  nnaddcl  11080  uzaddcl  11782  xaddass  12117  fztp  12435  seradd  12883  expadd  12942  bernneq  13030  faclbnd6  13126  hashgadd  13204  swrds2  13731  clim2ser  14429  clim2ser2  14430  summolem3  14489  isumsplit  14616  fsumcube  14835  odd2np1lem  15111  prmlem0  15859  cnaddablx  18317  cnaddabl  18318  zaddablx  18321  cncrng  19815  cnlmod  22986  pjthlem1  23254  ptolemy  24293  bcp1ctr  25049  cnaddabloOLD  27564  pjhthlem1  28378  dnibndlem5  32597  mblfinlem2  33577  mogoldbblem  41954  nnsgrp  42142  2zrngasgrp  42265
  Copyright terms: Public domain W3C validator