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