Metamath Proof Explorer

Theorem 6p4e10

Description: 6 + 4 = 10. (Contributed by NM, 5-Feb-2007) (Revised by Stanislas Polu, 7-Apr-2020) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion 6p4e10 
|- ( 6 + 4 ) = ; 1 0

Proof

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