Theorem 1e0p1 9713

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 9316	. 2 |- ( 0 + 1 ) = 1
2	1	eqcomi 2235	1 |- 1 = ( 0 + 1 )

Syntax hints:   = wceq 1398  (class class class)co 6028   0cc0 8092   1c1 8093   + caddc 8095

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213  ax-1cn 8185  ax-icn 8187  ax-addcl 8188  ax-mulcl 8190  ax-addcom 8192  ax-i2m1 8197  ax-0id 8200

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  6p5e11  9744  7p4e11  9747  8p3e11  9752  9p2e11  9758  fz1ssfz0  10414  fz0to3un2pr  10420  fzo01  10524  bcp1nk  11087  pfx1  11350  arisum2  12140  ege2le3  12312  ef4p  12335  efgt1p2  12336  efgt1p  12337  bitsmod  12597  prmdiv  12887  ennnfonelem1  13108  mulgnn0p1  13800  dveflem  15537  lgsdir2lem3  15849  lgseisenlem1  15889