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 859 | 1 ⊢ (𝜑 ∨ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 844 |
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 845 |
This theorem is referenced by: exmidd 893 pm5.62 1016 pm5.63 1017 pm4.83 1022 cases 1040 xpima 6085 ssfi 8956 ixxun 13095 trclfvg 14726 mreexexd 17357 lgsquadlem2 26529 numclwwlk3lem2 28748 elimifd 30886 elim2ifim 30888 iocinif 31102 hasheuni 32053 voliune 32197 volfiniune 32198 bnj1304 32799 fvresval 33741 wl-cases2-dnf 35671 cnambfre 35825 tsim1 36288 rp-isfinite6 41125 or3or 41631 uunT1 42400 onfrALTVD 42511 ax6e2ndeqVD 42529 ax6e2ndeqALT 42551 testable 46504 |
Copyright terms: Public domain | W3C validator |