Theorem addlid 8253

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 8106	. . 3 ⊢ 0 ∈ ℂ
2		addcom 8251	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 425	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addrid 8252	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
5	3, 4	eqtr3d 2244	1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965  0cc0 7967   + caddc 7970

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-17 1552  ax-ial 1560  ax-ext 2191  ax-1cn 8060  ax-icn 8062  ax-addcl 8063  ax-mulcl 8065  ax-addcom 8067  ax-i2m1 8072  ax-0id 8075

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-clel 2205

This theorem is referenced by:  readdcan  8254  addlidi  8257  addlidd  8264  cnegexlem1  8289  cnegexlem2  8290  addcan  8294  negneg  8364  fz0to4untppr  10288  fzo0addel  10361  fzoaddel2  10363  divfl0  10483  modqid  10538  swrdspsleq  11165  swrds1  11166  sumrbdclem  11854  summodclem2a  11858  fisum0diag2  11924  eftlub  12167  gcdid  12473  cncrng  14498  ptolemy  15463