Theorem addridi 8476

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

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8184  0cc0 8186   + caddc 8189

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

This theorem is used by:  1p0e1  9430  9p1e10  9791  num0u  9799  numnncl2  9816  decrmanc  9850  decaddi  9853  decaddci  9854  decmul1  9857  decmulnc  9860  fsumrelem  12264  demoivreALT  12567  decsplit0  13237  37prm  13265  43prm  13266  139prm  13268  163prm  13269  317prm  13270  631prm  13271  1259lem2  13273  1259lem3  13274  1259lem4  13275  1259lem5  13276  ballotfilemth  13340  sinhalfpilem  16030  efipi  16040  log2ublem3  16235  log2ublog2  16236