Theorem gbpart9

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

	Ref	Expression
Assertion	gbpart9	⊢ 9 = ( ( 3 + 3 ) + 3 )

Proof

Step	Hyp	Ref	Expression
1		3p3e6	⊢ ( 3 + 3 ) = 6
2	1	oveq1i	⊢ ( ( 3 + 3 ) + 3 ) = ( 6 + 3 )
3		6p3e9	⊢ ( 6 + 3 ) = 9
4	2 3	eqtr2i	⊢ 9 = ( ( 3 + 3 ) + 3 )