![]() |
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 895 pm5.62 1018 pm5.63 1019 pm4.83 1024 cases 1042 xpima 6182 fvresval 7355 ssfi 9173 ixxun 13340 trclfvg 14962 mreexexd 17592 lgsquadlem2 26884 numclwwlk3lem2 29637 elimifd 31775 elim2ifim 31777 iocinif 31992 hasheuni 33083 voliune 33227 volfiniune 33228 bnj1304 33830 wl-cases2-dnf 36381 cnambfre 36536 tsim1 36998 rp-isfinite6 42269 or3or 42774 uunT1 43541 onfrALTVD 43652 ax6e2ndeqVD 43670 ax6e2ndeqALT 43692 testable 47847 |
Copyright terms: Public domain | W3C validator |