Theorem evenprm2

Description: A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020)

	Ref	Expression
Assertion	evenprm2	|- ( P e. Prime -> ( P e. Even <-> P = 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2a1	|- ( P = 2 -> ( P e. Prime -> ( P e. Even -> P = 2 ) ) )
2		df-ne	|- ( P =/= 2 <-> -. P = 2 )
3	2	biimpri	|- ( -. P = 2 -> P =/= 2 )
4	3	anim2i	|- ( ( P e. Prime /\ -. P = 2 ) -> ( P e. Prime /\ P =/= 2 ) )
5	4	ancoms	|- ( ( -. P = 2 /\ P e. Prime ) -> ( P e. Prime /\ P =/= 2 ) )
6		eldifsn	|- ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
7	5 6	sylibr	|- ( ( -. P = 2 /\ P e. Prime ) -> P e. ( Prime \ { 2 } ) )
8		oddprmALTV	|- ( P e. ( Prime \ { 2 } ) -> P e. Odd )
9		oddneven	|- ( P e. Odd -> -. P e. Even )
10	9	pm2.21d	|- ( P e. Odd -> ( P e. Even -> P = 2 ) )
11	7 8 10	3syl	|- ( ( -. P = 2 /\ P e. Prime ) -> ( P e. Even -> P = 2 ) )
12	11	ex	|- ( -. P = 2 -> ( P e. Prime -> ( P e. Even -> P = 2 ) ) )
13	1 12	pm2.61i	|- ( P e. Prime -> ( P e. Even -> P = 2 ) )
14		2evenALTV	|- 2 e. Even
15		eleq1	|- ( P = 2 -> ( P e. Even <-> 2 e. Even ) )
16	14 15	mpbiri	|- ( P = 2 -> P e. Even )
17	13 16	impbid1	|- ( P e. Prime -> ( P e. Even <-> P = 2 ) )