Metamath Proof Explorer

Theorem oddprmuzge3

Description: A prime number which is odd is an integer greater than or equal to 3. (Contributed by AV, 20-Jul-2020) (Proof shortened by AV, 21-Aug-2021)

Ref Expression
Assertion oddprmuzge3 
|- ( ( P e. Prime /\ P e. Odd ) -> P e. ( ZZ>= ` 3 ) )

Proof

Step Hyp Ref Expression
1 oddprmne2 
 |-  ( ( P e. Prime /\ P e. Odd ) <-> P e. ( Prime \ { 2 } ) )
2 oddprmge3 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) )
3 1 2 sylbi 
 |-  ( ( P e. Prime /\ P e. Odd ) -> P e. ( ZZ>= ` 3 ) )