Theorem nneoiALTV

Description: A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001) (Revised by AV, 19-Jun-2020)

	Ref	Expression
Hypothesis	nneoiALTV.1	⊢ 𝑁 ∈ ℕ
Assertion	nneoiALTV	⊢ ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd )

Proof

Step	Hyp	Ref	Expression
1		nneoiALTV.1	⊢ 𝑁 ∈ ℕ
2		nneoALTV	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) )
3	1 2	ax-mp	⊢ ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd )