Metamath Proof Explorer


Theorem 4p3e7

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

Ref Expression
Assertion 4p3e7
|- ( 4 + 3 ) = 7

Proof

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