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

Theorem addid2 7600
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 7459 . . 3 0 ∈ ℂ
2 addcom 7598 . . 3 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
31, 2mpan2 416 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4 addid1 7599 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
53, 4eqtr3d 2122 1 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  wcel 1438  (class class class)co 5634  cc 7327  0cc0 7329   + caddc 7332
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 7417  ax-icn 7419  ax-addcl 7420  ax-mulcl 7422  ax-addcom 7424  ax-i2m1 7429  ax-0id 7432
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  readdcan  7601  addid2i  7604  addid2d  7611  cnegexlem1  7636  cnegexlem2  7637  addcan  7641  negneg  7711  fzoaddel2  9569  divfl0  9668  modqid  9721  isumrblem  10729  isummolem2a  10735  fisum0diag2  10804  gcdid  11070
  Copyright terms: Public domain W3C validator