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 )