Theorem exmid 895

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 863	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∨ wo 848

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 849

This theorem is referenced by:  exmidd  896  pm5.62  1021  pm5.63  1022  pm4.83  1027  cases  1043  xpima  6140  fvresval  7306  ssfi  9100  ixxun  13305  trclfvg  14968  mreexexd  17605  lgsquadlem2  27358  numclwwlk3lem2  30469  elimifd  32628  elim2ifim  32630  iocinif  32869  hasheuni  34245  voliune  34389  volfiniune  34390  bnj1304  34977  wl-cases2-dnf  37851  cnambfre  38003  tsim1  38465  rp-isfinite6  43963  or3or  44468  uunT1  45224  onfrALTVD  45335  ax6e2ndeqVD  45353  ax6e2ndeqALT  45375  testable  50287