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	$$⊢\left(P\in \mathbb{P}\wedge P\in \mathrm{Odd}\right)\to P\in {\mathbb{Z}}_{\ge 3}$$

Proof

Step	Hyp	Ref	Expression
1		oddprmne2	$$⊢\left(P\in \mathbb{P}\wedge P\in \mathrm{Odd}\right)\leftrightarrow P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
2		oddprmge3	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to P\in {\mathbb{Z}}_{\ge 3}$$
3	1 2	sylbi	$$⊢\left(P\in \mathbb{P}\wedge P\in \mathrm{Odd}\right)\to P\in {\mathbb{Z}}_{\ge 3}$$