Theorem addridi 8475

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 8471	. 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 8183  0cc0 8185   + caddc 8188

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

This theorem is used by:  1p0e1  9429  9p1e10  9789  num0u  9797  numnncl2  9814  decrmanc  9848  decaddi  9851  decaddci  9852  decmul1  9855  decmulnc  9858  fsumrelem  12262  demoivreALT  12565  decsplit0  13235  37prm  13263  43prm  13264  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  ballotfilemth  13338  sinhalfpilem  16035  efipi  16045  log2ublem3  16240  log2ublog2  16241