Theorem addid2d 8121

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

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addlid 8110	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1363   ∈ wcel 2158  (class class class)co 5888  ℂcc 7823  0cc0 7825   + caddc 7828

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-1cn 7918  ax-icn 7920  ax-addcl 7921  ax-mulcl 7923  ax-addcom 7925  ax-i2m1 7930  ax-0id 7933

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  negeu  8162  ltadd2  8390  subge0  8446  sublt0d  8541  un0addcl  9223  lincmb01cmp  10017  modsumfzodifsn  10410  rennim  11025  max0addsup  11242  fsumsplit  11429  sumsplitdc  11454  fisum0diag2  11469  isumsplit  11513  arisum2  11521  efaddlem  11696  eftlub  11712  ef4p  11716  moddvds  11820  gcdaddm  11999  gcdmultipled  12008  bezoutlemb  12015  pcmpt  12355  mulgnn0dir  13045  limcimolemlt  14429  dvcnp2cntop  14459  dvmptcmulcn  14479  dveflem  14483  dvef  14484  sin0pilem1  14498  sin2kpi  14528  cos2kpi  14529  coshalfpim  14540  sinkpi  14564