Metamath Proof Explorer

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 )