Theorem oddn2prm

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

	Ref	Expression
Assertion	oddn2prm	|- ( N e. ( Prime \ { 2 } ) -> -. 2 || N )

Proof

Step	Hyp	Ref	Expression
1		nnoddn2prm	|- ( N e. ( Prime \ { 2 } ) -> ( N e. NN /\ -. 2 || N ) )
2	1	simprd	|- ( N e. ( Prime \ { 2 } ) -> -. 2 || N )