Theorem addlidd 8334

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035  0cc0 8037   + caddc 8040

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2212  ax-1cn 8130  ax-icn 8132  ax-addcl 8133  ax-mulcl 8135  ax-addcom 8137  ax-i2m1 8142  ax-0id 8145

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-clel 2226

This theorem is referenced by:  negeu  8375  ltadd2  8604  subge0  8660  sublt0d  8755  un0addcl  9440  lincmb01cmp  10243  modsumfzodifsn  10664  ccatlid  11192  swrdfv0  11244  swrdpfx  11297  pfxpfx  11298  cats1un  11311  swrdccatin2  11319  cats1fvnd  11355  rennim  11585  max0addsup  11802  fsumsplit  11991  sumsplitdc  12016  fisum0diag2  12031  isumsplit  12075  arisum2  12083  efaddlem  12258  eftlub  12274  ef4p  12278  moddvds  12383  gcdaddm  12578  gcdmultipled  12587  bezoutlemb  12594  pcmpt  12939  4sqlem11  12997  mulgnn0dir  13762  limcimolemlt  15417  dvcnp2cntop  15452  dvmptcmulcn  15474  dveflem  15479  dvef  15480  plymullem1  15501  sin0pilem1  15534  sin2kpi  15564  cos2kpi  15565  coshalfpim  15576  sinkpi  15600