Theorem gbpart8

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

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

Proof

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$$