![]() |
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 862 | 1 ⊢ (𝜑 ∨ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 847 |
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 207 df-or 848 |
This theorem is referenced by: exmidd 895 pm5.62 1020 pm5.63 1021 pm4.83 1026 cases 1042 xpima 6204 fvresval 7378 ssfi 9212 ixxun 13400 trclfvg 15051 mreexexd 17693 lgsquadlem2 27440 numclwwlk3lem2 30413 elimifd 32564 elim2ifim 32566 iocinif 32790 hasheuni 34066 voliune 34210 volfiniune 34211 bnj1304 34812 wl-cases2-dnf 37493 cnambfre 37655 tsim1 38117 rp-isfinite6 43508 or3or 44013 uunT1 44778 onfrALTVD 44889 ax6e2ndeqVD 44907 ax6e2ndeqALT 44929 testable 49031 |
Copyright terms: Public domain | W3C validator |