Theorem addlidd 8312

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013  0cc0 8015   + caddc 8018

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8108  ax-icn 8110  ax-addcl 8111  ax-mulcl 8113  ax-addcom 8115  ax-i2m1 8120  ax-0id 8123

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  negeu  8353  ltadd2  8582  subge0  8638  sublt0d  8733  un0addcl  9418  lincmb01cmp  10216  modsumfzodifsn  10635  ccatlid  11159  swrdfv0  11207  swrdpfx  11260  pfxpfx  11261  cats1un  11274  swrdccatin2  11282  cats1fvnd  11318  rennim  11534  max0addsup  11751  fsumsplit  11939  sumsplitdc  11964  fisum0diag2  11979  isumsplit  12023  arisum2  12031  efaddlem  12206  eftlub  12222  ef4p  12226  moddvds  12331  gcdaddm  12526  gcdmultipled  12535  bezoutlemb  12542  pcmpt  12887  4sqlem11  12945  mulgnn0dir  13710  limcimolemlt  15359  dvcnp2cntop  15394  dvmptcmulcn  15416  dveflem  15421  dvef  15422  plymullem1  15443  sin0pilem1  15476  sin2kpi  15506  cos2kpi  15507  coshalfpim  15518  sinkpi  15542