Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > 2bornot2b  Unicode version 
Description: The law of excluded middle. Act III, Theorem 1 of Shakespeare, Hamlet, Prince of Denmark (1602). Its author leaves its proof as an exercise for the reader  "To be, or not to be: that is the question"  starting a trend that has become standard in modernday textbooks, serving to make the frustrated reader feel inferior, or in some cases to mask the fact that the author does not know its solution. (Contributed by Prof. Loof Lirpa, 1Apr2006.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

2bornot2b 
Step  Hyp  Ref  Expression 

1  ax1 5  . . 3  
2  ax1 5  . . 3  
3  1, 2  mpd 14  . 2 
4  dfor 359  . 2  
5  3, 4  mpbir 200  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wo 357 class class class wbr 4023 cmul 8742 c2 9795 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 dfor 359 
Copyright terms: Public domain  W3C validator 