Metamath Proof Explorer

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 
|- N e. NN
Assertion nneoiALTV 
|- ( N e. Even <-> -. N e. Odd )

Proof

Step Hyp Ref Expression
1 nneoiALTV.1 
 |-  N e. NN
2 nneoALTV 
 |-  ( N e. NN -> ( N e. Even <-> -. N e. Odd ) )
3 1 2 ax-mp 
 |-  ( N e. Even <-> -. N e. Odd )