Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2bornot2b | Structured version Visualization version GIF 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 modern-day 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, 1-Apr-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
2bornot2b | ⊢ (2 · 𝐵 ∨ ¬ 2 · 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 | . . 3 ⊢ (¬ 2 · 𝐵 → (2 · 𝐵 → ¬ 2 · 𝐵)) | |
2 | ax-1 6 | . . 3 ⊢ (¬ 2 · 𝐵 → ((2 · 𝐵 → ¬ 2 · 𝐵) → ¬ 2 · 𝐵)) | |
3 | 1, 2 | mpd 15 | . 2 ⊢ (¬ 2 · 𝐵 → ¬ 2 · 𝐵) |
4 | df-or 845 | . 2 ⊢ ((2 · 𝐵 ∨ ¬ 2 · 𝐵) ↔ (¬ 2 · 𝐵 → ¬ 2 · 𝐵)) | |
5 | 3, 4 | mpbir 234 | 1 ⊢ (2 · 𝐵 ∨ ¬ 2 · 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 844 class class class wbr 5033 · cmul 10535 2c2 11684 |
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 210 df-or 845 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |