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

Theorem addid1d 7142
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 7131 . 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 5499   CCcc 6868   0cc0 6870    + caddc 6873
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-0id 6973
This theorem is referenced by:  subsub2  7218  negsub  7238  ltaddpos  7425  addge01  7445  add20  7447  apreap  7554  nnge1  7913  nnnn0addcl  8184  un0addcl  8187  peano2z  8253  zaddcl  8257  uzaddcl  8501  fzosubel3  9019  expadd  9175  reim0b  9340  rereb  9341  immul2  9358  resqrexlemcalc3  9492  resqrexlemnm  9494
  Copyright terms: Public domain W3C validator