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

Theorem addid2d 7695
Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
addid2d (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addid2 7684 . 2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
31, 2syl 14 1 (𝜑 → (0 + 𝐴) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1290  wcel 1439  (class class class)co 5668  cc 7411  0cc0 7413   + caddc 7416
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 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071  ax-1cn 7501  ax-icn 7503  ax-addcl 7504  ax-mulcl 7506  ax-addcom 7508  ax-i2m1 7513  ax-0id 7516
This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085
This theorem is referenced by:  negeu  7736  ltadd2  7960  subge0  8016  sublt0d  8110  un0addcl  8769  lincmb01cmp  9483  modsumfzodifsn  9866  rennim  10498  max0addsup  10715  fsumsplit  10864  sumsplitdc  10889  fisum0diag2  10904  isumsplit  10948  arisum2  10956  efaddlem  11027  eftlub  11043  ef4p  11047  moddvds  11146  gcdaddm  11316  bezoutlemb  11330
  Copyright terms: Public domain W3C validator