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

Theorem addass 7165
Description: Alias for ax-addass 7140, for naming consistency with addassi 7189. (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 7140 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 920    = wceq 1285    e. wcel 1434  (class class class)co 5543   CCcc 7041    + caddc 7046
This theorem was proved from axioms:  ax-addass 7140
This theorem is referenced by:  addassi  7189  addassd  7203  add12  7333  add32  7334  add32r  7335  add4  7336  nnaddcl  8126  uzaddcl  8755  fztp  9171  iseradd  9559  expadd  9615  bernneq  9690  faclbnd6  9768  resqrexlemover  10034  clim2iser  10313  clim2iser2  10314  odd2np1lem  10416
  Copyright terms: Public domain W3C validator