Theorem addridi 8470

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

Hypothesis

Ref	Expression
mul.1	|- A e. CC

Assertion

Ref	Expression
addridi	|- ( A + 0 ) = A

Proof of Theorem addridi

Step	Hyp	Ref	Expression
1		mul.1	. 2 |- A e. CC
2		addrid 8466	. 2 |- ( A e. CC -> ( A + 0 ) = A )
3	1, 2	ax-mp 5	1 |- ( A + 0 ) = A

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   0cc0 8180   + caddc 8183

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

This theorem is used by:  1p0e1  9423  9p1e10  9784  num0u  9792  numnncl2  9809  decrmanc  9843  decaddi  9846  decaddci  9847  decmul1  9850  decmulnc  9853  fsumrelem  12256  demoivreALT  12559  decsplit0  13229  37prm  13257  43prm  13258  139prm  13260  163prm  13261  317prm  13262  631prm  13263  1259lem2  13265  1259lem3  13266  1259lem4  13267  1259lem5  13268  ballotfilemth  13332  sinhalfpilem  15945  efipi  15955  log2ublem3  16145  log2ublog2  16146