Metamath Proof Explorer


Theorem gboodd

Description: An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion gboodd Z GoldbachOdd Z Odd

Proof

Step Hyp Ref Expression
1 gbogbow Z GoldbachOdd Z GoldbachOddW
2 gbowodd Z GoldbachOddW Z Odd
3 1 2 syl Z GoldbachOdd Z Odd