Theorem addlid 8465

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 8463	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 429	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addrid 8464	. 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  8466  addlidi  8469  addlidd  8476  cnegexlem1  8501  cnegexlem2  8502  addcan  8506  negneg  8576  fz0to4untppr  10533  fzo0addel  10608  fzoaddel2  10610  divfl0  10733  modqid  10788  swrdspsleq  11441  swrds1  11442  sumrbdclem  12146  summodclem2a  12150  fisum0diag2  12216  eftlub  12459  gcdid  12765  cncrng  14908  ptolemy  15928