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

Metamath Proof Explorer

Theorem gbpart11

Description: The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020)

		Ref	Expression
	Assertion	gbpart11	$⊢ 11 = 3 + 3 + 5$

Step	Hyp	Ref	Expression
1		3p3e6	$⊢ 3 + 3 = 6$
2	1	oveq1i	$⊢ 3 + 3 + 5 = 6 + 5$
3		6p5e11	$⊢ 6 + 5 = 11$
4	2 3	eqtr2i	$⊢ 11 = 3 + 3 + 5$