Theorem addlidd 8428

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130  0cc0 8132   + caddc 8135

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8225  ax-icn 8227  ax-addcl 8228  ax-mulcl 8230  ax-addcom 8232  ax-i2m1 8237  ax-0id 8240

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

This theorem is referenced by:  negeu  8469  ltadd2  8698  subge0  8754  sublt0d  8849  un0addcl  9534  lincmb01cmp  10342  modsumfzodifsn  10765  bcm1n  11139  ccatlid  11302  swrdfv0  11354  swrdpfx  11407  pfxpfx  11408  cats1un  11421  swrdccatin2  11429  cats1fvnd  11465  rennim  11695  max0addsup  11912  fsumsplit  12101  sumsplitdc  12126  fisum0diag2  12141  isumsplit  12185  arisum2  12193  efaddlem  12368  eftlub  12384  ef4p  12388  moddvds  12493  gcdaddm  12688  gcdmultipled  12697  bezoutlemb  12704  pcmpt  13049  4sqlem11  13107  mulgnn0dir  13890  limcimolemlt  15578  dvcnp2cntop  15613  dvmptcmulcn  15635  dveflem  15640  dvef  15641  plymullem1  15662  sin0pilem1  15695  sin2kpi  15725  cos2kpi  15726  coshalfpim  15737  sinkpi  15761