Metamath Proof Explorer


Theorem 5p4e9

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

Ref Expression
Assertion 5p4e9
|- ( 5 + 4 ) = 9

Proof

Step Hyp Ref Expression
1 df-4
 |-  4 = ( 3 + 1 )
2 1 oveq2i
 |-  ( 5 + 4 ) = ( 5 + ( 3 + 1 ) )
3 5cn
 |-  5 e. CC
4 3cn
 |-  3 e. CC
5 ax-1cn
 |-  1 e. CC
6 3 4 5 addassi
 |-  ( ( 5 + 3 ) + 1 ) = ( 5 + ( 3 + 1 ) )
7 2 6 eqtr4i
 |-  ( 5 + 4 ) = ( ( 5 + 3 ) + 1 )
8 df-9
 |-  9 = ( 8 + 1 )
9 5p3e8
 |-  ( 5 + 3 ) = 8
10 9 oveq1i
 |-  ( ( 5 + 3 ) + 1 ) = ( 8 + 1 )
11 8 10 eqtr4i
 |-  9 = ( ( 5 + 3 ) + 1 )
12 7 11 eqtr4i
 |-  ( 5 + 4 ) = 9