Metamath Proof Explorer


Theorem zeneo

Description: No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of Apostol p. 28. This variant of zneo follows immediately from the fact that a contradiction implies anything, see pm2.21i . (Contributed by AV, 22-Jun-2021)

Ref Expression
Assertion zeneo AB2A¬2BAB

Proof

Step Hyp Ref Expression
1 nbrne1 2A¬2BAB
2 1 a1i AB2A¬2BAB