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

Theorem addid2d 8109
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 addlid 8098 . 2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
31, 2syl 14 1 (𝜑 → (0 + 𝐴) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  wcel 2148  (class class class)co 5877  cc 7811  0cc0 7813   + caddc 7816
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7906  ax-icn 7908  ax-addcl 7909  ax-mulcl 7911  ax-addcom 7913  ax-i2m1 7918  ax-0id 7921
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173
This theorem is referenced by:  negeu  8150  ltadd2  8378  subge0  8434  sublt0d  8529  un0addcl  9211  lincmb01cmp  10005  modsumfzodifsn  10398  rennim  11013  max0addsup  11230  fsumsplit  11417  sumsplitdc  11442  fisum0diag2  11457  isumsplit  11501  arisum2  11509  efaddlem  11684  eftlub  11700  ef4p  11704  moddvds  11808  gcdaddm  11987  gcdmultipled  11996  bezoutlemb  12003  pcmpt  12343  mulgnn0dir  13018  limcimolemlt  14172  dvcnp2cntop  14202  dvmptcmulcn  14222  dveflem  14226  dvef  14227  sin0pilem1  14241  sin2kpi  14271  cos2kpi  14272  coshalfpim  14283  sinkpi  14307
  Copyright terms: Public domain W3C validator