Theorem addlidd 8476

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 8465	. 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  8517  ltadd2  8747  subge0  8803  sublt0d  8899  un0addcl  9598  lincmb01cmp  10407  modsumfzodifsn  10835  bcm1n  11209  ccatlid  11376  swrdfv0  11428  swrdpfx  11481  pfxpfx  11482  cats1un  11495  swrdccatin2  11503  cats1fvnd  11539  rennim  11770  max0addsup  11987  fsumsplit  12176  sumsplitdc  12201  fisum0diag2  12216  isumsplit  12260  arisum2  12268  efaddlem  12443  eftlub  12459  ef4p  12463  moddvds  12568  gcdaddm  12763  gcdmultipled  12772  bezoutlemb  12779  pcmpt  13124  4sqlem11  13182  mulgnn0dir  13957  limcimolemlt  15767  dvcnp2cntop  15802  dvmptcmulcn  15824  dveflem  15829  dvef  15830  plymullem1  15851  sin0pilem1  15885  sin2kpi  15915  cos2kpi  15916  coshalfpim  15927  sinkpi  15951  logfac  16001