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 856 | 1 ⊢ (𝜑 ∨ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 841 |
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 208 df-or 842 |
This theorem is referenced by: exmidd 889 pm5.62 1012 pm5.63 1013 pm4.83 1018 cases 1034 xpima 6032 ixxun 12742 trclfvg 14363 mreexexd 16907 lgsquadlem2 25884 numclwwlk3lem2 28090 elimifd 30225 elim2ifim 30227 iocinif 30430 hasheuni 31243 voliune 31387 volfiniune 31388 bnj1304 31990 fvresval 32907 wl-cases2-dnf 34634 cnambfre 34821 tsim1 35289 rp-isfinite6 39762 or3or 40249 uunT1 40991 onfrALTVD 41102 ax6e2ndeqVD 41120 ax6e2ndeqALT 41142 testable 44829 |
Copyright terms: Public domain | W3C validator |