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

Theorem addid1d 7879
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 7868 . 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 1316    e. wcel 1465  (class class class)co 5742   CCcc 7586   0cc0 7588    + caddc 7591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 7696
This theorem is referenced by:  subsub2  7958  negsub  7978  ltaddneg  8154  ltaddpos  8182  addge01  8202  add20  8204  apreap  8317  nnge1  8711  nnnn0addcl  8975  un0addcl  8978  peano2z  9058  zaddcl  9062  uzaddcl  9349  xaddid1  9613  fzosubel3  9941  expadd  10303  faclbnd6  10458  omgadd  10516  reim0b  10602  rereb  10603  immul2  10620  resqrexlemcalc3  10756  resqrexlemnm  10758  max0addsup  10959  fsumsplit  11144  sumsplitdc  11169  bezoutlema  11614  cosmpi  12824  sinppi  12825  sinhalfpip  12828  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator