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