Theorem oddprmne2

Description: Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021)

	Ref	Expression
Assertion	oddprmne2	|- ( ( P e. Prime /\ P e. Odd ) <-> P e. ( Prime \ { 2 } ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	|- ( P e. Prime -> P e. ZZ )
2		zeo2ALTV	|- ( P e. ZZ -> ( P e. Even <-> -. P e. Odd ) )
3	1 2	syl	|- ( P e. Prime -> ( P e. Even <-> -. P e. Odd ) )
4		evenprm2	|- ( P e. Prime -> ( P e. Even <-> P = 2 ) )
5	3 4	bitr3d	|- ( P e. Prime -> ( -. P e. Odd <-> P = 2 ) )
6		nne	|- ( -. P =/= 2 <-> P = 2 )
7	5 6	bitr4di	|- ( P e. Prime -> ( -. P e. Odd <-> -. P =/= 2 ) )
8	7	con4bid	|- ( P e. Prime -> ( P e. Odd <-> P =/= 2 ) )
9	8	pm5.32i	|- ( ( P e. Prime /\ P e. Odd ) <-> ( P e. Prime /\ P =/= 2 ) )
10		eldifsn	|- ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
11	9 10	bitr4i	|- ( ( P e. Prime /\ P e. Odd ) <-> P e. ( Prime \ { 2 } ) )