Theorem 1e0p1 9768

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

Syntax hints:   = wceq 1398  (class class class)co 6058   0cc0 8143   1c1 8144   + caddc 8146

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 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-addcom 8243  ax-i2m1 8248  ax-0id 8251

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

This theorem is referenced by:  6p5e11  9799  7p4e11  9802  8p3e11  9807  9p2e11  9813  fz1ssfz0  10473  fz0to3un2pr  10479  fzo01  10583  bcp1nk  11149  pfx1  11420  arisum2  12210  ege2le3  12382  ef4p  12405  efgt1p2  12406  efgt1p  12407  bitsmod  12667  prmdiv  12957  ballotfilemii  13190  ballotfilem1c  13195  ennnfonelem1  13242  mulgnn0p1  13886  dveflem  15717  lgsdir2lem3  16029  lgseisenlem1  16069