![]() |
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 860 | 1 ⊢ (𝜑 ∨ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 845 |
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 206 df-or 846 |
This theorem is referenced by: exmidd 894 pm5.62 1017 pm5.63 1018 pm4.83 1023 cases 1041 xpima 6178 fvresval 7351 ssfi 9169 ixxun 13336 trclfvg 14958 mreexexd 17588 lgsquadlem2 26873 numclwwlk3lem2 29626 elimifd 31762 elim2ifim 31764 iocinif 31979 hasheuni 33071 voliune 33215 volfiniune 33216 bnj1304 33818 wl-cases2-dnf 36369 cnambfre 36524 tsim1 36986 rp-isfinite6 42254 or3or 42759 uunT1 43526 onfrALTVD 43637 ax6e2ndeqVD 43655 ax6e2ndeqALT 43677 testable 47800 |
Copyright terms: Public domain | W3C validator |