Theorem addlid 8417

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 8271	. . 3 ⊢ 0 ∈ ℂ
2		addcom 8415	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 425	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addrid 8416	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
5	3, 4	eqtr3d 2269	1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130  0cc0 8132   + caddc 8135

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8225  ax-icn 8227  ax-addcl 8228  ax-mulcl 8230  ax-addcom 8232  ax-i2m1 8237  ax-0id 8240

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  readdcan  8418  addlidi  8421  addlidd  8428  cnegexlem1  8453  cnegexlem2  8454  addcan  8458  negneg  8528  fz0to4untppr  10465  fzo0addel  10540  fzoaddel2  10542  divfl0  10663  modqid  10718  swrdspsleq  11367  swrds1  11368  sumrbdclem  12071  summodclem2a  12075  fisum0diag2  12141  eftlub  12384  gcdid  12690  cncrng  14766  ptolemy  15738