Theorem 1e0p1

Description: The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Assertion	1e0p1	⊢ 1 = ( 0 + 1 )

Proof

Step	Hyp	Ref	Expression
1		0p1e1	⊢ ( 0 + 1 ) = 1
2	1	eqcomi	⊢ 1 = ( 0 + 1 )