Metamath Proof Explorer


Theorem 6p6e12

Description: 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 6p6e12 6 + 6 = 12

Proof

Step Hyp Ref Expression
1 6nn0 6 0
2 5nn0 5 0
3 1nn0 1 0
4 df-6 6 = 5 + 1
5 df-2 2 = 1 + 1
6 6p5e11 6 + 5 = 11
7 1 2 3 4 5 6 6p5lem 6 + 6 = 12