Theorem addlidd 8477

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177  0cc0 8179   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-addcom 8279  ax-i2m1 8284  ax-0id 8287

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  negeu  8518  ltadd2  8748  subge0  8804  sublt0d  8900  un0addcl  9600  lincmb01cmp  10415  modsumfzodifsn  10846  bcm1n  11221  ccatlid  11388  swrdfv0  11440  swrdpfx  11493  pfxpfx  11494  cats1un  11507  swrdccatin2  11515  cats1fvnd  11551  rennim  11782  max0addsup  12000  fsumsplit  12190  sumsplitdc  12215  fisum0diag2  12230  isumsplit  12274  arisum2  12282  efaddlem  12457  eftlub  12473  ef4p  12477  moddvds  12582  gcdaddm  12777  gcdmultipled  12786  bezoutlemb  12793  pcmpt  13142  4sqlem11  13200  mulgnn0dir  14004  limcimolemlt  15814  dvcnp2cntop  15849  dvmptcmulcn  15871  dveflem  15876  dvef  15877  plymullem1  15898  sin0pilem1  15932  sin2kpi  15962  cos2kpi  15963  coshalfpim  15974  sinkpi  15998  logfac  16048  chtublem  16214