Theorem 2bornot2b 30930

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

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 16	. 2 ⊢ (¬ 2 · 𝐵 → ¬ 2 · 𝐵)
4		df-or 862	. 2 ⊢ ((2 · 𝐵 ∨ ¬ 2 · 𝐵) ↔ (¬ 2 · 𝐵 → ¬ 2 · 𝐵))
5	3, 4	mpbir 234	1 ⊢ (2 · 𝐵 ∨ ¬ 2 · 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861   class class class wbr 5107   · cmul 11132  2c2 12322

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by: (None)