Metamath Proof Explorer

Theorem gbeeven

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

Ref Expression
Assertion gbeeven 
|- ( Z e. GoldbachEven -> Z e. Even )

Proof

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