Theorem exmid 415

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

Syntax hints:   -. wn 3   \/ wo 368

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 370

This theorem is referenced by:  exmidd  416  pm5.62  914  pm5.63  915  pm4.83  920  4exmid  930  jaoi2OLD  960  cases  962  cases2  963  exmidneOLD  2659  xpima  5391  ixxun  11431  lgsquadlem2  22837  cusgrasizeindslem2  23561  ifbieq12d2  26082  elimifd  26083  elim2if  26084  elim2ifim  26085  iocinif  26243  hasheuni  26702  voliune  26812  volfiniune  26813  fvresval  27745  cnambfre  28611  tsim1  29112  testable  31507  uunT1  31868  onfrALTVD  31982  ax6e2ndeqVD  32000  ax6e2ndeqALT  32022  bnj1304  32168