Metamath Proof Explorer

Definition df-4

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

Ref Expression
Assertion df-4 
|- 4 = ( 3 + 1 )

Detailed syntax breakdown

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