Metamath Proof Explorer


Theorem 7p3e10

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

Ref Expression
Assertion 7p3e10 ( 7 + 3 ) = 1 0

Proof

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