Theorem addlid 8408

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 8262	. . 3 ⊢ 0 ∈ ℂ
2		addcom 8406	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 425	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addrid 8407	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
5	3, 4	eqtr3d 2267	1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121  0cc0 8123   + caddc 8126

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 2214  ax-1cn 8216  ax-icn 8218  ax-addcl 8219  ax-mulcl 8221  ax-addcom 8223  ax-i2m1 8228  ax-0id 8231

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  readdcan  8409  addlidi  8412  addlidd  8419  cnegexlem1  8444  cnegexlem2  8445  addcan  8449  negneg  8519  fz0to4untppr  10454  fzo0addel  10529  fzoaddel2  10531  divfl0  10652  modqid  10707  swrdspsleq  11352  swrds1  11353  sumrbdclem  12056  summodclem2a  12060  fisum0diag2  12126  eftlub  12369  gcdid  12675  cncrng  14704  ptolemy  15676