Theorem addlidd 8484

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 8473	. 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 6088  ℂcc 8184  0cc0 8186   + caddc 8189

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 8279  ax-icn 8281  ax-addcl 8282  ax-mulcl 8284  ax-addcom 8286  ax-i2m1 8291  ax-0id 8294

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

This theorem is used by:  negeu  8525  ltadd2  8755  subge0  8811  sublt0d  8907  un0addcl  9608  lincmb01cmp  10423  modsumfzodifsn  10855  bcm1n  11230  ccatlid  11397  swrdfv0  11449  swrdpfx  11502  pfxpfx  11503  cats1un  11516  swrdccatin2  11524  cats1fvnd  11560  rennim  11791  max0addsup  12009  fsumsplit  12200  sumsplitdc  12225  fisum0diag2  12240  isumsplit  12284  arisum2  12292  efaddlem  12467  eftlub  12483  ef4p  12487  moddvds  12592  gcdaddm  12787  gcdmultipled  12796  bezoutlemb  12803  pcmpt  13152  4sqlem11  13210  mulgnn0dir  14015  limcimolemlt  15902  dvcnp2cntop  15937  dvmptcmulcn  15959  dveflem  15964  dvef  15965  plymullem1  15986  sin0pilem1  16020  sin2kpi  16050  cos2kpi  16051  coshalfpim  16062  sinkpi  16086  logfac  16138  chtublem  16307