Metamath Proof Explorer


Theorem 8p3e11

Description: 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion 8p3e11 ( 8 + 3 ) = 1 1

Proof

Step Hyp Ref Expression
1 8nn0 8 ∈ ℕ0
2 2nn0 2 ∈ ℕ0
3 0nn0 0 ∈ ℕ0
4 df-3 3 = ( 2 + 1 )
5 1e0p1 1 = ( 0 + 1 )
6 8p2e10 ( 8 + 2 ) = 1 0
7 1 2 3 4 5 6 6p5lem ( 8 + 3 ) = 1 1