Theorem addid2d 7695

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

Syntax hints:   → wi 4   = wceq 1290   ∈ wcel 1439  (class class class)co 5668  ℂcc 7411  0cc0 7413   + caddc 7416

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071  ax-1cn 7501  ax-icn 7503  ax-addcl 7504  ax-mulcl 7506  ax-addcom 7508  ax-i2m1 7513  ax-0id 7516

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085

This theorem is referenced by:  negeu  7736  ltadd2  7960  subge0  8016  sublt0d  8110  un0addcl  8769  lincmb01cmp  9483  modsumfzodifsn  9866  rennim  10498  max0addsup  10715  fsumsplit  10864  sumsplitdc  10889  fisum0diag2  10904  isumsplit  10948  arisum2  10956  efaddlem  11027  eftlub  11043  ef4p  11047  moddvds  11146  gcdaddm  11316  bezoutlemb  11330