Theorem gbpart7

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

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

Proof

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