Theorem 1e0p1 9642

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

Syntax hints:   = wceq 1395  (class class class)co 6013   0cc0 8022   1c1 8023   + caddc 8025

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 8115  ax-icn 8117  ax-addcl 8118  ax-mulcl 8120  ax-addcom 8122  ax-i2m1 8127  ax-0id 8130

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

This theorem is referenced by:  6p5e11  9673  7p4e11  9676  8p3e11  9681  9p2e11  9687  fz1ssfz0  10342  fz0to3un2pr  10348  fzo01  10451  bcp1nk  11014  pfx1  11274  arisum2  12050  ege2le3  12222  ef4p  12245  efgt1p2  12246  efgt1p  12247  bitsmod  12507  prmdiv  12797  ennnfonelem1  13018  mulgnn0p1  13710  dveflem  15440  lgsdir2lem3  15749  lgseisenlem1  15789