Theorem 1e0p1 9619

Description: The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
1e0p1	|- 1 = ( 0 + 1 )

Proof of Theorem 1e0p1

Step	Hyp	Ref	Expression
1		0p1e1 9224	. 2 |- ( 0 + 1 ) = 1
2	1	eqcomi 2233	1 |- 1 = ( 0 + 1 )

Syntax hints:   = wceq 1395  (class class class)co 6001   0cc0 7999   1c1 8000   + caddc 8002

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8092  ax-icn 8094  ax-addcl 8095  ax-mulcl 8097  ax-addcom 8099  ax-i2m1 8104  ax-0id 8107

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  6p5e11  9650  7p4e11  9653  8p3e11  9658  9p2e11  9664  fz1ssfz0  10313  fz0to3un2pr  10319  fzo01  10422  bcp1nk  10984  pfx1  11235  arisum2  12010  ege2le3  12182  ef4p  12205  efgt1p2  12206  efgt1p  12207  bitsmod  12467  prmdiv  12757  ennnfonelem1  12978  mulgnn0p1  13670  dveflem  15400  lgsdir2lem3  15709  lgseisenlem1  15749