Theorem oddn2prm

Description: A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021)

	Ref	Expression
Assertion	oddn2prm	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \neg 2\parallel N$$

Proof

Step	Hyp	Ref	Expression
1		nnoddn2prm	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(N\in \mathbb{N}\wedge \neg 2\parallel N\right)$$
2	1	simprd	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \neg 2\parallel N$$