Theorem addlidd 8425

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

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

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 8222  ax-icn 8224  ax-addcl 8225  ax-mulcl 8227  ax-addcom 8229  ax-i2m1 8234  ax-0id 8237

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

This theorem is referenced by:  negeu  8466  ltadd2  8695  subge0  8751  sublt0d  8846  un0addcl  9531  lincmb01cmp  10339  modsumfzodifsn  10762  bcm1n  11135  ccatlid  11298  swrdfv0  11350  swrdpfx  11403  pfxpfx  11404  cats1un  11417  swrdccatin2  11425  cats1fvnd  11461  rennim  11691  max0addsup  11908  fsumsplit  12097  sumsplitdc  12122  fisum0diag2  12137  isumsplit  12181  arisum2  12189  efaddlem  12364  eftlub  12380  ef4p  12384  moddvds  12489  gcdaddm  12684  gcdmultipled  12693  bezoutlemb  12700  pcmpt  13045  4sqlem11  13103  mulgnn0dir  13886  limcimolemlt  15546  dvcnp2cntop  15581  dvmptcmulcn  15603  dveflem  15608  dvef  15609  plymullem1  15630  sin0pilem1  15663  sin2kpi  15693  cos2kpi  15694  coshalfpim  15705  sinkpi  15729