Theorem addid2d 8110

Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addid2d	⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addlid 8099	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5878  ℂcc 7812  0cc0 7814   + caddc 7817

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7907  ax-icn 7909  ax-addcl 7910  ax-mulcl 7912  ax-addcom 7914  ax-i2m1 7919  ax-0id 7922

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  negeu  8151  ltadd2  8379  subge0  8435  sublt0d  8530  un0addcl  9212  lincmb01cmp  10006  modsumfzodifsn  10399  rennim  11014  max0addsup  11231  fsumsplit  11418  sumsplitdc  11443  fisum0diag2  11458  isumsplit  11502  arisum2  11510  efaddlem  11685  eftlub  11701  ef4p  11705  moddvds  11809  gcdaddm  11988  gcdmultipled  11997  bezoutlemb  12004  pcmpt  12344  mulgnn0dir  13023  limcimolemlt  14294  dvcnp2cntop  14324  dvmptcmulcn  14344  dveflem  14348  dvef  14349  sin0pilem1  14363  sin2kpi  14393  cos2kpi  14394  coshalfpim  14405  sinkpi  14429