Metamath Proof Explorer

Theorem evenprm2

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

Ref Expression
Assertion evenprm2 ⊢P∈ℙ→P∈Even↔P=2

Proof

Step Hyp Ref Expression
1 2a1 ⊢P=2→P∈ℙ→P∈Even→P=2
2 df-ne ⊢P≠2↔¬P=2
3 2 biimpri ⊢¬P=2→P≠2
4 3 anim2i ⊢P∈ℙ∧¬P=2→P∈ℙ∧P≠2
5 4 ancoms ⊢¬P=2∧P∈ℙ→P∈ℙ∧P≠2
6 eldifsn ⊢P∈ℙ∖2↔P∈ℙ∧P≠2
7 5 6 sylibr ⊢¬P=2∧P∈ℙ→P∈ℙ∖2
8 oddprmALTV ⊢P∈ℙ∖2→P∈Odd
9 oddneven ⊢P∈Odd→¬P∈Even
10 9 pm2.21d ⊢P∈Odd→P∈Even→P=2
11 7 8 10 3syl ⊢¬P=2∧P∈ℙ→P∈Even→P=2
12 11 ex ⊢¬P=2→P∈ℙ→P∈Even→P=2
13 1 12 pm2.61i ⊢P∈ℙ→P∈Even→P=2
14 2evenALTV ⊢2∈Even
15 eleq1 ⊢P=2→P∈Even↔2∈Even
16 14 15 mpbiri ⊢P=2→P∈Even
17 13 16 impbid1 ⊢P∈ℙ→P∈Even↔P=2