Theorem 00id 8100

Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
00id	|- ( 0 + 0 ) = 0

Proof of Theorem 00id

Step	Hyp	Ref	Expression
1		0cn 7951	. 2 |- 0 e. CC
2		addid1 8097	. 2 |- ( 0 e. CC -> ( 0 + 0 ) = 0 )
3	1, 2	ax-mp 5	1 |- ( 0 + 0 ) = 0

Syntax hints:   = wceq 1353   e. wcel 2148  (class class class)co 5877   CCcc 7811   0cc0 7813   + caddc 7816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7906  ax-icn 7908  ax-addcl 7909  ax-mulcl 7911  ax-i2m1 7918  ax-0id 7921

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  negdii  8243  addgt0  8407  addgegt0  8408  addgtge0  8409  addge0  8410  add20  8433  recexaplem2  8611  crap0  8917  iap0  9144  decaddm10  9444  10p10e20  9480  ser0  10516  bcpasc  10748  abs00ap  11073  fsumadd  11416  fsumrelem  11481  arisum  11508  bezoutr1  12036  nnnn0modprm0  12257  pcaddlem  12340  cnfld0  13550  1kp2ke3k  14561