Theorem addid2 7894

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

Assertion

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

Proof of Theorem addid2

Step	Hyp	Ref	Expression
1		0cn 7751	. . 3 ⊢ 0 ∈ ℂ
2		addcom 7892	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 421	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addid1 7893	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
5	3, 4	eqtr3d 2172	1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  (class class class)co 5767  ℂcc 7611  0cc0 7613   + caddc 7616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1cn 7706  ax-icn 7708  ax-addcl 7709  ax-mulcl 7711  ax-addcom 7713  ax-i2m1 7718  ax-0id 7721

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  readdcan  7895  addid2i  7898  addid2d  7905  cnegexlem1  7930  cnegexlem2  7931  addcan  7935  negneg  8005  fzoaddel2  9963  divfl0  10062  modqid  10115  sumrbdclem  11138  summodclem2a  11143  fisum0diag2  11209  eftlub  11385  gcdid  11663  ptolemy  12894