Theorem exmid 908

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 23	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	orri 876	1 ⊢ (𝜑 ∨ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ∨ wo 861

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:  exmidd  909  pm5.62  1036  pm5.63  1037  pm4.83  1042  cases  1058  xpima  6187  fvresval  7394  ssfi  9219  ixxun  13522  trclfvg  15200  mreexexd  17854  lgsquadlem2  27741  numclwwlk3lem2  31018  cgrainag  33093  elimifd  33214  elim2ifim  33216  iocinif  33446  hasheuni  34800  voliune  34945  volfiniune  34946  bnj1304  35532  wl-cases2-dnf  38649  cnambfre  38791  tsim1  39265  rp-isfinite6  44722  or3or  45226  uunT1  45964  onfrALTVD  46075  ax6e2ndeqVD  46093  ax6e2ndeqALT  46115  testable  51250