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 210 df-or 847 |
This theorem is referenced by: exmidd 895 pm5.62 1018 pm5.63 1019 pm4.83 1024 cases 1042 xpima 6014 ssfi 8772 ixxun 12837 trclfvg 14464 mreexexd 17022 lgsquadlem2 26117 numclwwlk3lem2 28321 elimifd 30460 elim2ifim 30462 iocinif 30677 hasheuni 31623 voliune 31767 volfiniune 31768 bnj1304 32370 fvresval 33313 wl-cases2-dnf 35294 cnambfre 35448 tsim1 35911 rp-isfinite6 40679 or3or 41177 uunT1 41938 onfrALTVD 42049 ax6e2ndeqVD 42067 ax6e2ndeqALT 42089 testable 45957 |
Copyright terms: Public domain | W3C validator |