ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  00id GIF version

Theorem 00id 7316
Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
00id (0 + 0) = 0

Proof of Theorem 00id
StepHypRef Expression
1 0cn 7173 . 2 0 ∈ ℂ
2 addid1 7313 . 2 (0 ∈ ℂ → (0 + 0) = 0)
31, 2ax-mp 7 1 (0 + 0) = 0
Colors of variables: wff set class
Syntax hints:   = wceq 1285  wcel 1434  (class class class)co 5543  cc 7041  0cc0 7043   + caddc 7046
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1cn 7131  ax-icn 7133  ax-addcl 7134  ax-mulcl 7136  ax-i2m1 7143  ax-0id 7146
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  negdii  7459  addgt0  7619  addgegt0  7620  addgtge0  7621  addge0  7622  add20  7645  recexaplem2  7809  crap0  8102  iap0  8321  decaddm10  8616  10p10e20  8652  iser0  9568  bcpasc  9790  abs00ap  10086  bezoutr1  10566  1kp2ke3k  10713
  Copyright terms: Public domain W3C validator