This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 10p10e20

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

		Ref	Expression
	Assertion	10p10e20	$⊢ 10 + 10 = 20$

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		0nn0	$⊢ 0 \in ℕ_{0}$
3		eqid	$⊢ 10 = 10$
4		1p1e2	$⊢ 1 + 1 = 2$
5		00id	$⊢ 0 + 0 = 0$
6	1 2 1 2 3 3 4 5	decadd	$⊢ 10 + 10 = 20$