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

Theorem addid1d 7162
Description:  0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
addid1d  |-  ( ph  ->  ( A  +  0 )  =  A )

Proof of Theorem addid1d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addid1 7151 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
31, 2syl 14 1  |-  ( ph  ->  ( A  +  0 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243    e. wcel 1393  (class class class)co 5512   CCcc 6887   0cc0 6889    + caddc 6892
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-0id 6992
This theorem is referenced by:  subsub2  7239  negsub  7259  ltaddpos  7447  addge01  7467  add20  7469  apreap  7578  nnge1  7937  nnnn0addcl  8212  un0addcl  8215  peano2z  8281  zaddcl  8285  uzaddcl  8529  fzosubel3  9052  expadd  9297  reim0b  9462  rereb  9463  immul2  9480  resqrexlemcalc3  9614  resqrexlemnm  9616
  Copyright terms: Public domain W3C validator