Metamath Proof Explorer


Theorem 4p2e6

Description: 4 + 2 = 6. (Contributed by NM, 11-May-2004)

Ref Expression
Assertion 4p2e6 ( 4 + 2 ) = 6

Proof

Step Hyp Ref Expression
1 df-2 2 = ( 1 + 1 )
2 1 oveq2i ( 4 + 2 ) = ( 4 + ( 1 + 1 ) )
3 4cn 4 ∈ ℂ
4 ax-1cn 1 ∈ ℂ
5 3 4 4 addassi ( ( 4 + 1 ) + 1 ) = ( 4 + ( 1 + 1 ) )
6 2 5 eqtr4i ( 4 + 2 ) = ( ( 4 + 1 ) + 1 )
7 df-5 5 = ( 4 + 1 )
8 7 oveq1i ( 5 + 1 ) = ( ( 4 + 1 ) + 1 )
9 6 8 eqtr4i ( 4 + 2 ) = ( 5 + 1 )
10 df-6 6 = ( 5 + 1 )
11 9 10 eqtr4i ( 4 + 2 ) = 6