Metamath Proof Explorer


Theorem 5p2e7

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

Ref Expression
Assertion 5p2e7
|- ( 5 + 2 ) = 7

Proof

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