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$$