![]() |
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 861 | 1 ⊢ (𝜑 ∨ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 846 |
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 847 |
This theorem is referenced by: exmidd 894 pm5.62 1017 pm5.63 1018 pm4.83 1023 cases 1041 xpima 6180 fvresval 7360 ssfi 9189 ixxun 13364 trclfvg 14986 mreexexd 17619 lgsquadlem2 27301 numclwwlk3lem2 30181 elimifd 32319 elim2ifim 32321 iocinif 32533 hasheuni 33640 voliune 33784 volfiniune 33785 bnj1304 34386 wl-cases2-dnf 36915 cnambfre 37076 tsim1 37538 rp-isfinite6 42871 or3or 43376 uunT1 44142 onfrALTVD 44253 ax6e2ndeqVD 44271 ax6e2ndeqALT 44293 testable 48156 |
Copyright terms: Public domain | W3C validator |