Theorem exmid 894

Description: Law of excluded middle, also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic. In intuitionistic logic, if this statement is true for some 𝜑, then 𝜑 is decidable. (Contributed by NM, 29-Dec-1992.)

Assertion

Ref	Expression
exmid	⊢ (𝜑 ∨ ¬ 𝜑)

Proof of Theorem exmid

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	orri 862	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  exmidd  895  pm5.62  1020  pm5.63  1021  pm4.83  1026  cases  1042  xpima  6155  fvresval  7333  ssfi  9137  ixxun  13322  trclfvg  14981  mreexexd  17609  lgsquadlem2  27292  numclwwlk3lem2  30313  elimifd  32472  elim2ifim  32474  iocinif  32704  hasheuni  34075  voliune  34219  volfiniune  34220  bnj1304  34809  wl-cases2-dnf  37500  cnambfre  37662  tsim1  38124  rp-isfinite6  43507  or3or  44012  uunT1  44769  onfrALTVD  44880  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  testable  49789