ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addass Unicode version

Theorem addass 7904
Description: Alias for ax-addass 7876, for naming consistency with addassi 7928. (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 7876 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 973    = wceq 1348    e. wcel 2141  (class class class)co 5853   CCcc 7772    + caddc 7777
This theorem was proved from axioms:  ax-addass 7876
This theorem is referenced by:  addassi  7928  addassd  7942  add12  8077  add32  8078  add32r  8079  add4  8080  nnaddcl  8898  uzaddcl  9545  xaddass  9826  fztp  10034  ser3add  10461  expadd  10518  bernneq  10596  faclbnd6  10678  resqrexlemover  10974  clim2ser  11300  clim2ser2  11301  summodclem3  11343  isumsplit  11454  cvgratnnlemseq  11489  odd2np1lem  11831  ptolemy  13539
  Copyright terms: Public domain W3C validator