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

Theorem addid2 8029
Description: 0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
addid2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2
StepHypRef Expression
1 0cn 7883 . . 3 0 ∈ ℂ
2 addcom 8027 . . 3 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
31, 2mpan2 422 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4 addid1 8028 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
53, 4eqtr3d 2199 1 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1342  wcel 2135  (class class class)co 5837  cc 7743  0cc0 7745   + caddc 7748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146  ax-1cn 7838  ax-icn 7840  ax-addcl 7841  ax-mulcl 7843  ax-addcom 7845  ax-i2m1 7850  ax-0id 7853
This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160
This theorem is referenced by:  readdcan  8030  addid2i  8033  addid2d  8040  cnegexlem1  8065  cnegexlem2  8066  addcan  8070  negneg  8140  fz0to4untppr  10050  fzoaddel2  10119  divfl0  10222  modqid  10275  sumrbdclem  11308  summodclem2a  11312  fisum0diag2  11378  eftlub  11621  gcdid  11908  ptolemy  13312
  Copyright terms: Public domain W3C validator