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

Theorem addid2i 7623
Description:  0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
Hypothesis
Ref Expression
mul.1  |-  A  e.  CC
Assertion
Ref Expression
addid2i  |-  ( 0  +  A )  =  A

Proof of Theorem addid2i
StepHypRef Expression
1 mul.1 . 2  |-  A  e.  CC
2 addid2 7619 . 2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
31, 2ax-mp 7 1  |-  ( 0  +  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1289    e. wcel 1438  (class class class)co 5652   CCcc 7346   0cc0 7348    + caddc 7351
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1cn 7436  ax-icn 7438  ax-addcl 7439  ax-mulcl 7441  ax-addcom 7443  ax-i2m1 7448  ax-0id 7451
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  ine0  7870  inelr  8059  muleqadd  8135  0p1e1  8534  iap0  8637  num0h  8886  nummul1c  8923  decrmac  8932  decmul1  8938  fz0tp  9531  fzo0to3tp  9626  rei  10329  imi  10330  resqrexlemover  10439  ef01bndlem  11043  ex-fac  11610
  Copyright terms: Public domain W3C validator