Metamath Proof Explorer

Theorem gbpart7

Description: The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion gbpart7 
|- 7 = ( ( 2 + 2 ) + 3 )

Proof

Step Hyp Ref Expression
1 2p2e4 
 |-  ( 2 + 2 ) = 4
2 1 oveq1i 
 |-  ( ( 2 + 2 ) + 3 ) = ( 4 + 3 )
3 4p3e7 
 |-  ( 4 + 3 ) = 7
4 2 3 eqtr2i 
 |-  7 = ( ( 2 + 2 ) + 3 )