Theorem oddprmne2

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

	Ref	Expression
Assertion	oddprmne2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ ( ℙ ∖ { 2 } ) )

Proof

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