Theorem exmid 417

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 ph, then ph is decideable. (Contributed by NM, 29-Dec-1992.)

Assertion

Ref	Expression
exmid	|- ( ph \/ -. ph )

Proof of Theorem exmid

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( -. ph -> -. ph )
2	1	orri 378	1 |- ( ph \/ -. ph )

Syntax hints:   -. wn 3   \/ wo 370

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 189  df-or 372

This theorem is referenced by:  exmidd  418  pm5.62  935  pm5.63  936  pm4.83  941  4exmid  951  cases  983  xpima  5282  ixxun  11658  trclfvg  13091  lgsquadlem2  24295  cusgrasizeindslem2  25214  ifbieq12d2  28171  elimifd  28172  elim2ifim  28174  iocinif  28375  hasheuni  28918  voliune  29064  volfiniune  29065  bnj1304  29643  fvresval  30420  wl-cases2-dnf  31862  cnambfre  32001  tsim1  32384  rp-isfinite6  36175  uunT1  37177  onfrALTVD  37298  ax6e2ndeqVD  37316  ax6e2ndeqALT  37338  testable  40643