MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2bornot2b Structured version   Visualization version   GIF version

Theorem 2bornot2b 28170
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.)
Assertion
Ref Expression
2bornot2b (2 · 𝐵 ∨ ¬ 2 · 𝐵)

Proof of Theorem 2bornot2b
StepHypRef Expression
1 ax-1 6 . . 3 (¬ 2 · 𝐵 → (2 · 𝐵 → ¬ 2 · 𝐵))
2 ax-1 6 . . 3 (¬ 2 · 𝐵 → ((2 · 𝐵 → ¬ 2 · 𝐵) → ¬ 2 · 𝐵))
31, 2mpd 15 . 2 (¬ 2 · 𝐵 → ¬ 2 · 𝐵)
4 df-or 842 . 2 ((2 · 𝐵 ∨ ¬ 2 · 𝐵) ↔ (¬ 2 · 𝐵 → ¬ 2 · 𝐵))
53, 4mpbir 232 1 (2 · 𝐵 ∨ ¬ 2 · 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 841   class class class wbr 5057   · cmul 10530  2c2 11680
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 208  df-or 842
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator