Theorem addid2 7901

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 7758	. . 3 ⊢ 0 ∈ ℂ
2		addcom 7899	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 421	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addid1 7900	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
5	3, 4	eqtr3d 2174	1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618  0cc0 7620   + caddc 7623

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 2121  ax-1cn 7713  ax-icn 7715  ax-addcl 7716  ax-mulcl 7718  ax-addcom 7720  ax-i2m1 7725  ax-0id 7728

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  readdcan  7902  addid2i  7905  addid2d  7912  cnegexlem1  7937  cnegexlem2  7938  addcan  7942  negneg  8012  fzoaddel2  9970  divfl0  10069  modqid  10122  sumrbdclem  11146  summodclem2a  11150  fisum0diag2  11216  eftlub  11396  gcdid  11674  ptolemy  12905