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

Metamath Proof Explorer

Theorem gbpart8

Description: The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020)

		Ref	Expression
	Assertion	gbpart8	$⊢ 8 = 3 + 5$

Step	Hyp	Ref	Expression
1		5cn	$⊢ 5 \in ℂ$
2		3cn	$⊢ 3 \in ℂ$
3		5p3e8	$⊢ 5 + 3 = 8$
4	1 2 3	addcomli	$⊢ 3 + 5 = 8$
5	4	eqcomi	$⊢ 8 = 3 + 5$