Metamath Proof Explorer


Theorem gbpart8

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

Ref Expression
Assertion gbpart8 8 = 3 + 5

Proof

Step Hyp Ref Expression
1 5cn 5
2 3cn 3
3 5p3e8 5 + 3 = 8
4 1 2 3 addcomli 3 + 5 = 8
5 4 eqcomi 8 = 3 + 5