Theorem addlidd 8329

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030  0cc0 8032   + caddc 8035

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-addcom 8132  ax-i2m1 8137  ax-0id 8140

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  negeu  8370  ltadd2  8599  subge0  8655  sublt0d  8750  un0addcl  9435  lincmb01cmp  10238  modsumfzodifsn  10659  ccatlid  11184  swrdfv0  11236  swrdpfx  11289  pfxpfx  11290  cats1un  11303  swrdccatin2  11311  cats1fvnd  11347  rennim  11564  max0addsup  11781  fsumsplit  11970  sumsplitdc  11995  fisum0diag2  12010  isumsplit  12054  arisum2  12062  efaddlem  12237  eftlub  12253  ef4p  12257  moddvds  12362  gcdaddm  12557  gcdmultipled  12566  bezoutlemb  12573  pcmpt  12918  4sqlem11  12976  mulgnn0dir  13741  limcimolemlt  15391  dvcnp2cntop  15426  dvmptcmulcn  15448  dveflem  15453  dvef  15454  plymullem1  15475  sin0pilem1  15508  sin2kpi  15538  cos2kpi  15539  coshalfpim  15550  sinkpi  15574