Metamath Proof Explorer

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 ∈ ℙ ∧ P ∈ Odd ↔ P ∈ ℙ ∖ 2

Proof

Step Hyp Ref Expression
1 prmz ⊢ P ∈ ℙ → P ∈ ℤ
2 zeo2ALTV ⊢ P ∈ ℤ → P ∈ Even ↔ ¬ P ∈ Odd
3 1 2 syl ⊢ P ∈ ℙ → P ∈ Even ↔ ¬ P ∈ Odd
4 evenprm2 ⊢ P ∈ ℙ → P ∈ Even ↔ P = 2
5 3 4 bitr3d ⊢ P ∈ ℙ → ¬ P ∈ Odd ↔ P = 2
6 nne ⊢ ¬ P ≠ 2 ↔ P = 2
7 5 6 bitr4di ⊢ P ∈ ℙ → ¬ P ∈ Odd ↔ ¬ P ≠ 2
8 7 con4bid ⊢ P ∈ ℙ → P ∈ Odd ↔ P ≠ 2
9 8 pm5.32i ⊢ P ∈ ℙ ∧ P ∈ Odd ↔ P ∈ ℙ ∧ P ≠ 2
10 eldifsn ⊢ P ∈ ℙ ∖ 2 ↔ P ∈ ℙ ∧ P ≠ 2
11 9 10 bitr4i ⊢ P ∈ ℙ ∧ P ∈ Odd ↔ P ∈ ℙ ∖ 2