Theorem addlidd 8229

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930  0cc0 7932   + caddc 7935

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188  ax-1cn 8025  ax-icn 8027  ax-addcl 8028  ax-mulcl 8030  ax-addcom 8032  ax-i2m1 8037  ax-0id 8040

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

This theorem is referenced by:  negeu  8270  ltadd2  8499  subge0  8555  sublt0d  8650  un0addcl  9335  lincmb01cmp  10132  modsumfzodifsn  10548  ccatlid  11070  swrdfv0  11115  swrdpfx  11166  pfxpfx  11167  rennim  11357  max0addsup  11574  fsumsplit  11762  sumsplitdc  11787  fisum0diag2  11802  isumsplit  11846  arisum2  11854  efaddlem  12029  eftlub  12045  ef4p  12049  moddvds  12154  gcdaddm  12349  gcdmultipled  12358  bezoutlemb  12365  pcmpt  12710  4sqlem11  12768  mulgnn0dir  13532  limcimolemlt  15180  dvcnp2cntop  15215  dvmptcmulcn  15237  dveflem  15242  dvef  15243  plymullem1  15264  sin0pilem1  15297  sin2kpi  15327  cos2kpi  15328  coshalfpim  15339  sinkpi  15363