Metamath Proof Explorer

Theorem gbowodd

Description: A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020)

Ref Expression
Assertion gbowodd 
|- ( Z e. GoldbachOddW -> Z e. Odd )

Proof

Step Hyp Ref Expression
1 isgbow 
 |-  ( Z e. GoldbachOddW <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) )
2 1 simplbi 
 |-  ( Z e. GoldbachOddW -> Z e. Odd )