![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exmid | Structured version Visualization version GIF version |
Description: Law of excluded middle, also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic. In intuitionistic logic, if this statement is true for some 𝜑, then 𝜑 is decidable. (Contributed by NM, 29-Dec-1992.) |
Ref | Expression |
---|---|
exmid | ⊢ (𝜑 ∨ ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (¬ 𝜑 → ¬ 𝜑) | |
2 | 1 | orri 893 | 1 ⊢ (𝜑 ∨ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 878 |
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 199 df-or 879 |
This theorem is referenced by: exmidd 924 pm5.62 1047 pm5.63 1048 pm4.83 1053 cases 1069 xpima 5817 ixxun 12479 trclfvg 14133 mreexexd 16661 lgsquadlem2 25519 numclwwlk3lem2 27788 elimifd 29899 elim2ifim 29901 iocinif 30079 hasheuni 30681 voliune 30826 volfiniune 30827 bnj1304 31425 fvresval 32196 wl-cases2-dnf 33833 cnambfre 33994 tsim1 34470 rp-isfinite6 38698 or3or 39152 uunT1 39827 onfrALTVD 39938 ax6e2ndeqVD 39956 ax6e2ndeqALT 39978 testable 43435 |
Copyright terms: Public domain | W3C validator |