Theorem 1e0p1 9580

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

Syntax hints:   = wceq 1373  (class class class)co 5967  0cc0 7960  1c1 7961   + caddc 7963

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1cn 8053  ax-icn 8055  ax-addcl 8056  ax-mulcl 8058  ax-addcom 8060  ax-i2m1 8065  ax-0id 8068

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  6p5e11  9611  7p4e11  9614  8p3e11  9619  9p2e11  9625  fz1ssfz0  10274  fz0to3un2pr  10280  fzo01  10382  bcp1nk  10944  pfx1  11194  arisum2  11925  ege2le3  12097  ef4p  12120  efgt1p2  12121  efgt1p  12122  bitsmod  12382  prmdiv  12672  ennnfonelem1  12893  mulgnn0p1  13584  dveflem  15313  lgsdir2lem3  15622  lgseisenlem1  15662