| 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 863 | 1 ⊢ (𝜑 ∨ ¬ 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∨ wo 848 |
| 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 849 |
| This theorem is referenced by: exmidd 896 pm5.62 1021 pm5.63 1022 pm4.83 1027 cases 1043 xpima 6202 fvresval 7378 ssfi 9213 ixxun 13403 trclfvg 15054 mreexexd 17691 lgsquadlem2 27425 numclwwlk3lem2 30403 elimifd 32556 elim2ifim 32558 iocinif 32783 hasheuni 34086 voliune 34230 volfiniune 34231 bnj1304 34833 wl-cases2-dnf 37513 cnambfre 37675 tsim1 38137 rp-isfinite6 43531 or3or 44036 uunT1 44800 onfrALTVD 44911 ax6e2ndeqVD 44929 ax6e2ndeqALT 44951 testable 49319 |
| Copyright terms: Public domain | W3C validator |