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

Metamath Proof Explorer

Theorem gbpart7

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

		Ref	Expression
	Assertion	gbpart7	$⊢ 7 = 2 + 2 + 3$

Step	Hyp	Ref	Expression
1		2p2e4	$⊢ 2 + 2 = 4$
2	1	oveq1i	$⊢ 2 + 2 + 3 = 4 + 3$
3		4p3e7	$⊢ 4 + 3 = 7$
4	2 3	eqtr2i	$⊢ 7 = 2 + 2 + 3$