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

Theorem addid2i 8131
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 addlid 8127 . 2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
31, 2ax-mp 5 1 (0 + 𝐴) = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1364  wcel 2160  (class class class)co 5897  cc 7840  0cc0 7842   + caddc 7845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1cn 7935  ax-icn 7937  ax-addcl 7938  ax-mulcl 7940  ax-addcom 7942  ax-i2m1 7947  ax-0id 7950
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185
This theorem is referenced by:  ine0  8382  inelr  8572  muleqadd  8656  0p1e1  9064  iap0  9173  num0h  9426  nummul1c  9463  decrmac  9472  decmul1  9478  fz0tp  10154  fz0to4untppr  10156  fzo0to3tp  10251  rei  10943  imi  10944  resqrexlemover  11054  ef01bndlem  11799  efhalfpi  14697  sinq34lt0t  14729  ex-fac  14958
  Copyright terms: Public domain W3C validator