Metamath Proof Explorer

Definition df-2

Description: Define the number 2. (Contributed by NM, 27-May-1999)

Ref Expression
Assertion df-2 
|- 2 = ( 1 + 1 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c2 
 |-  2
1 c1 
 |-  1
2 caddc 
 |-  +
3 1 1 2 co 
 |-  ( 1 + 1 )
4 0 3 wceq 
 |-  2 = ( 1 + 1 )