Metamath Proof Explorer

Definition df-8

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

Ref Expression
Assertion df-8 
|- 8 = ( 7 + 1 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c8 
 |-  8
1 c7 
 |-  7
2 caddc 
 |-  +
3 c1 
 |-  1
4 1 3 2 co 
 |-  ( 7 + 1 )
5 0 4 wceq 
 |-  8 = ( 7 + 1 )