Theorem addlid 8466

Description: 0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
addlid	⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Proof of Theorem addlid

Step	Hyp	Ref	Expression
1		0cn 8318	. . 3 ⊢ 0 ∈ ℂ
2		addcom 8464	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 429	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addrid 8465	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
5	3, 4	eqtr3d 2273	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:  readdcan  8467  addlidi  8470  addlidd  8477  cnegexlem1  8502  cnegexlem2  8503  addcan  8507  negneg  8577  fz0to4untppr  10541  fzo0addel  10616  fzoaddel2  10618  divfl0  10744  modqid  10799  swrdspsleq  11453  swrds1  11454  sumrbdclem  12160  summodclem2a  12164  fisum0diag2  12230  eftlub  12473  gcdid  12779  cncrng  14955  ptolemy  15975