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 15  . 2 
4  dfor 360  . 2  
5  3, 4  mpbir 201  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wo 358 class class class wbr 4167 cmul 8942 c2 9995 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfor 360 
Copyright terms: Public domain  W3C validator 