Theorem addridi 8462

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 8458	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 + 0) = 𝐴

Syntax hints:   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171  0cc0 8173   + caddc 8176

This theorem was proved from axioms:  ax-mp 5  ax-0id 8281

This theorem is referenced by:  1p0e1  9403  9p1e10  9762  num0u  9770  numnncl2  9782  decrmanc  9816  decaddi  9819  decaddci  9820  decmul1  9823  decmulnc  9826  fsumrelem  12221  demoivreALT  12524  decsplit0  13189  ballotfilemth  13264  sinhalfpilem  15875  efipi  15885  log2ublem3  16068  log2ublog2  16069