Metamath Proof Explorer


Theorem 5p3e8

Description: 5 + 3 = 8. (Contributed by NM, 11-May-2004)

Ref Expression
Assertion 5p3e8 ( 5 + 3 ) = 8

Proof

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