Metamath Proof Explorer

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 )