![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exmid | Structured version Visualization version Unicode 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 ![]() ![]() |
Ref | Expression |
---|---|
exmid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | orri 378 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 189 df-or 372 |
This theorem is referenced by: exmidd 418 pm5.62 935 pm5.63 936 pm4.83 941 4exmid 951 cases 983 xpima 5282 ixxun 11658 trclfvg 13091 lgsquadlem2 24295 cusgrasizeindslem2 25214 ifbieq12d2 28171 elimifd 28172 elim2ifim 28174 iocinif 28375 hasheuni 28918 voliune 29064 volfiniune 29065 bnj1304 29643 fvresval 30420 wl-cases2-dnf 31862 cnambfre 32001 tsim1 32384 rp-isfinite6 36175 uunT1 37177 onfrALTVD 37298 ax6e2ndeqVD 37316 ax6e2ndeqALT 37338 testable 40643 |
Copyright terms: Public domain | W3C validator |