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

Theorem addass 8840
Description: Alias for ax-addass 8818, for naming consistency with addassi 8861. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addass  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 8818 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    = wceq 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756
This theorem is referenced by:  addassi  8861  addassd  8873  00id  9003  addid2  9011  add12  9041  add32  9042  add4  9043  nnaddcl  9784  nneo  10111  uzaddcl  10291  xaddass  10585  fztp  10857  seradd  11104  expadd  11160  bernneq  11243  faclbnd6  11328  hashgadd  11375  swrds2  11576  clim2ser  12144  clim2ser2  12145  summolem3  12203  bcxmaslem2  12309  isumsplit  12315  odd2np1lem  12602  prmlem0  13123  cnaddablx  15174  cnaddabl  15175  zaddablx  15176  cncrng  16411  pjthlem1  18817  ptolemy  19880  bcp1ctr  20534  gxnn0add  20957  cnaddablo  21033  pjhthlem1  21986  fsumcube  24867  mslb1  25710  2wsms  25711  stoweidlem13  27865  wlkdvspthlem  28365
This theorem was proved from axioms:  ax-addass 8818
  Copyright terms: Public domain W3C validator