Theorem 1e0p1 9455

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 9063	. 2 ⊢ (0 + 1) = 1
2	1	eqcomi 2193	1 ⊢ 1 = (0 + 1)

Syntax hints:   = wceq 1364  (class class class)co 5896  0cc0 7841  1c1 7842   + caddc 7844

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1cn 7934  ax-icn 7936  ax-addcl 7937  ax-mulcl 7939  ax-addcom 7941  ax-i2m1 7946  ax-0id 7949

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  6p5e11  9486  7p4e11  9489  8p3e11  9494  9p2e11  9500  fz1ssfz0  10147  fz0to3un2pr  10153  fzo01  10246  bcp1nk  10774  arisum2  11539  ege2le3  11711  ef4p  11734  efgt1p2  11735  efgt1p  11736  prmdiv  12267  ennnfonelem1  12458  mulgnn0p1  13073  dveflem  14644  lgsdir2lem3  14889  lgseisenlem1  14908