Theorem addid2d 8048

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		addid2 8037	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136  (class class class)co 5842  ℂcc 7751  0cc0 7753   + caddc 7756

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1cn 7846  ax-icn 7848  ax-addcl 7849  ax-mulcl 7851  ax-addcom 7853  ax-i2m1 7858  ax-0id 7861

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  negeu  8089  ltadd2  8317  subge0  8373  sublt0d  8468  un0addcl  9147  lincmb01cmp  9939  modsumfzodifsn  10331  rennim  10944  max0addsup  11161  fsumsplit  11348  sumsplitdc  11373  fisum0diag2  11388  isumsplit  11432  arisum2  11440  efaddlem  11615  eftlub  11631  ef4p  11635  moddvds  11739  gcdaddm  11917  gcdmultipled  11926  bezoutlemb  11933  pcmpt  12273  limcimolemlt  13273  dvcnp2cntop  13303  dvmptcmulcn  13323  dveflem  13327  dvef  13328  sin0pilem1  13342  sin2kpi  13372  cos2kpi  13373  coshalfpim  13384  sinkpi  13408