Theorem addridi 8469

Description: 0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)

Hypothesis

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
addridi	⊢ (𝐴 + 0) = 𝐴

Proof of Theorem addridi

Step	Hyp	Ref	Expression
1		mul.1	. 2 ⊢ 𝐴 ∈ ℂ
2		addrid 8465	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 + 0) = 𝐴

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177  0cc0 8179   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-0id 8287

This theorem is used by:  1p0e1  9422  9p1e10  9783  num0u  9791  numnncl2  9808  decrmanc  9842  decaddi  9845  decaddci  9846  decmul1  9849  decmulnc  9852  fsumrelem  12254  demoivreALT  12557  decsplit0  13227  37prm  13255  43prm  13256  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  ballotfilemth  13330  sinhalfpilem  15942  efipi  15952  log2ublem3  16142  log2ublog2  16143