Theorem gbpart11

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

	Ref	Expression
Assertion	gbpart11	⊢ ; 1 1 = ( ( 3 + 3 ) + 5 )

Proof

Step	Hyp	Ref	Expression
1		3p3e6	⊢ ( 3 + 3 ) = 6
2	1	oveq1i	⊢ ( ( 3 + 3 ) + 5 ) = ( 6 + 5 )
3		6p5e11	⊢ ( 6 + 5 ) = ; 1 1
4	2 3	eqtr2i	⊢ ; 1 1 = ( ( 3 + 3 ) + 5 )