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

Theorem addid1d 7376
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 7365 . 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 1285    e. wcel 1434  (class class class)co 5563   CCcc 7093   0cc0 7095    + caddc 7098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-0id 7198
This theorem is referenced by:  subsub2  7455  negsub  7475  ltaddneg  7647  ltaddpos  7675  addge01  7695  add20  7697  apreap  7806  nnge1  8181  nnnn0addcl  8437  un0addcl  8440  peano2z  8520  zaddcl  8524  uzaddcl  8807  fzosubel3  9334  expadd  9667  faclbnd6  9820  omgadd  9878  reim0b  9950  rereb  9951  immul2  9968  resqrexlemcalc3  10103  resqrexlemnm  10105  max0addsup  10306  bezoutlema  10595
  Copyright terms: Public domain W3C validator