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  6134  fvresval  7298  ssfi  9089  ixxun  13263  trclfvg  14924  mreexexd  17556  lgsquadlem2  27320  numclwwlk3lem2  30366  elimifd  32525  elim2ifim  32527  iocinif  32768  hasheuni  34119  voliune  34263  volfiniune  34264  bnj1304  34852  wl-cases2-dnf  37577  cnambfre  37728  tsim1  38190  rp-isfinite6  43635  or3or  44140  uunT1  44896  onfrALTVD  45007  ax6e2ndeqVD  45025  ax6e2ndeqALT  45047  testable  49925