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