Theorem addlidd 8264

Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addlidd	⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addlidd

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

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965  0cc0 7967   + caddc 7970

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-17 1552  ax-ial 1560  ax-ext 2191  ax-1cn 8060  ax-icn 8062  ax-addcl 8063  ax-mulcl 8065  ax-addcom 8067  ax-i2m1 8072  ax-0id 8075

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-clel 2205

This theorem is referenced by:  negeu  8305  ltadd2  8534  subge0  8590  sublt0d  8685  un0addcl  9370  lincmb01cmp  10167  modsumfzodifsn  10585  ccatlid  11107  swrdfv0  11152  swrdpfx  11205  pfxpfx  11206  cats1un  11219  swrdccatin2  11227  cats1fvnd  11263  rennim  11479  max0addsup  11696  fsumsplit  11884  sumsplitdc  11909  fisum0diag2  11924  isumsplit  11968  arisum2  11976  efaddlem  12151  eftlub  12167  ef4p  12171  moddvds  12276  gcdaddm  12471  gcdmultipled  12480  bezoutlemb  12487  pcmpt  12832  4sqlem11  12890  mulgnn0dir  13655  limcimolemlt  15303  dvcnp2cntop  15338  dvmptcmulcn  15360  dveflem  15365  dvef  15366  plymullem1  15387  sin0pilem1  15420  sin2kpi  15450  cos2kpi  15451  coshalfpim  15462  sinkpi  15486