Theorem addlid 8098

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 7951	. . 3 ⊢ 0 ∈ ℂ
2		addcom 8096	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
3	1, 2	mpan2 425	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4		addid1 8097	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
5	3, 4	eqtr3d 2212	1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811  0cc0 7813   + caddc 7816

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7906  ax-icn 7908  ax-addcl 7909  ax-mulcl 7911  ax-addcom 7913  ax-i2m1 7918  ax-0id 7921

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  readdcan  8099  addid2i  8102  addid2d  8109  cnegexlem1  8134  cnegexlem2  8135  addcan  8139  negneg  8209  fz0to4untppr  10126  fzoaddel2  10195  divfl0  10298  modqid  10351  sumrbdclem  11387  summodclem2a  11391  fisum0diag2  11457  eftlub  11700  gcdid  11989  cncrng  13502  ptolemy  14284