Theorem addlidd 8419

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121  0cc0 8123   + caddc 8126

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 2214  ax-1cn 8216  ax-icn 8218  ax-addcl 8219  ax-mulcl 8221  ax-addcom 8223  ax-i2m1 8228  ax-0id 8231

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

This theorem is referenced by:  negeu  8460  ltadd2  8689  subge0  8745  sublt0d  8840  un0addcl  9525  lincmb01cmp  10332  modsumfzodifsn  10754  ccatlid  11287  swrdfv0  11339  swrdpfx  11392  pfxpfx  11393  cats1un  11406  swrdccatin2  11414  cats1fvnd  11450  rennim  11680  max0addsup  11897  fsumsplit  12086  sumsplitdc  12111  fisum0diag2  12126  isumsplit  12170  arisum2  12178  efaddlem  12353  eftlub  12369  ef4p  12373  moddvds  12478  gcdaddm  12673  gcdmultipled  12682  bezoutlemb  12689  pcmpt  13034  4sqlem11  13092  mulgnn0dir  13858  limcimolemlt  15516  dvcnp2cntop  15551  dvmptcmulcn  15573  dveflem  15578  dvef  15579  plymullem1  15600  sin0pilem1  15633  sin2kpi  15663  cos2kpi  15664  coshalfpim  15675  sinkpi  15699