This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )