Theorem exmid 413

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 374	1 |- ( ph \/ -. ph )

Syntax hints:   -. wn 3   \/ wo 366

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 185  df-or 368

This theorem is referenced by:  exmidd  414  pm5.62  921  pm5.63  922  pm4.83  927  4exmid  937  cases  968  exmidneOLD  2588  xpima  5359  ixxun  11466  trclfvg  12853  lgsquadlem2  23747  cusgrasizeindslem2  24595  ifbieq12d2  27545  elimifd  27546  elim2ifim  27548  iocinif  27745  hasheuni  28233  voliune  28357  volfiniune  28358  fvresval  29363  wl-cases2-dnf  30135  cnambfre  30228  tsim1  30703  testable  33549  uunT1  33917  onfrALTVD  34038  ax6e2ndeqVD  34056  ax6e2ndeqALT  34078  bnj1304  34225  rp-isfinite6  38173