Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > zeo3 | Structured version Visualization version Unicode version |
Description: An integer is even or odd. With this representation of even and odd integers, this variant of zeo 11463 follows immediately from the law of excluded middle, see exmidd 432. (Contributed by AV, 17-Jun-2021.) |
Ref | Expression |
---|---|
zeo3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exmidd 432 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wo 383 wcel 1990 class class class wbr 4653 c2 11070 cz 11377 cdvds 14983 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-or 385 |
This theorem is referenced by: zeo5 15080 |
Copyright terms: Public domain | W3C validator |