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

Theorem addid2i 7822
Description: 0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
Hypothesis
Ref Expression
mul.1 𝐴 ∈ ℂ
Assertion
Ref Expression
addid2i (0 + 𝐴) = 𝐴

Proof of Theorem addid2i
StepHypRef Expression
1 mul.1 . 2 𝐴 ∈ ℂ
2 addid2 7818 . 2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
31, 2ax-mp 7 1 (0 + 𝐴) = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1312  wcel 1461  (class class class)co 5726  cc 7539  0cc0 7541   + caddc 7544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095  ax-1cn 7632  ax-icn 7634  ax-addcl 7635  ax-mulcl 7637  ax-addcom 7639  ax-i2m1 7644  ax-0id 7647
This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109
This theorem is referenced by:  ine0  8069  inelr  8258  muleqadd  8336  0p1e1  8738  iap0  8841  num0h  9091  nummul1c  9128  decrmac  9137  decmul1  9143  fz0tp  9788  fzo0to3tp  9883  rei  10558  imi  10559  resqrexlemover  10668  ef01bndlem  11308  ex-fac  12624
  Copyright terms: Public domain W3C validator