Theorem addlidd 8440

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141  0cc0 8143   + caddc 8146

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 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-addcom 8243  ax-i2m1 8248  ax-0id 8251

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

This theorem is referenced by:  negeu  8481  ltadd2  8711  subge0  8767  sublt0d  8862  un0addcl  9549  lincmb01cmp  10358  modsumfzodifsn  10785  bcm1n  11159  ccatlid  11322  swrdfv0  11374  swrdpfx  11427  pfxpfx  11428  cats1un  11441  swrdccatin2  11449  cats1fvnd  11485  rennim  11715  max0addsup  11932  fsumsplit  12121  sumsplitdc  12146  fisum0diag2  12161  isumsplit  12205  arisum2  12213  efaddlem  12388  eftlub  12404  ef4p  12408  moddvds  12513  gcdaddm  12708  gcdmultipled  12717  bezoutlemb  12724  pcmpt  13069  4sqlem11  13127  mulgnn0dir  13908  limcimolemlt  15658  dvcnp2cntop  15693  dvmptcmulcn  15715  dveflem  15720  dvef  15721  plymullem1  15742  sin0pilem1  15775  sin2kpi  15805  cos2kpi  15806  coshalfpim  15817  sinkpi  15841