Metamath Proof Explorer

Theorem gboodd

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

Ref Expression
Assertion gboodd 
|- ( Z e. GoldbachOdd -> Z e. Odd )

Proof

Step Hyp Ref Expression
1 gbogbow 
 |-  ( Z e. GoldbachOdd -> Z e. GoldbachOddW )
2 gbowodd 
 |-  ( Z e. GoldbachOddW -> Z e. Odd )
3 1 2 syl 
 |-  ( Z e. GoldbachOdd -> Z e. Odd )