Metamath Proof Explorer

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 )