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  921  pm5.63  922  pm4.83  927  4exmid  937  cases  968  cases2OLD  970  exmidneOLD  2647  xpima  5435  ixxun  11549  lgsquadlem2  23495  cusgrasizeindslem2  24339  ifbieq12d2  27285  elimifd  27286  elim2ifim  27288  iocinif  27457  hasheuni  27957  voliune  28067  volfiniune  28068  fvresval  29165  cnambfre  30031  tsim1  30505  testable  32925  uunT1  33285  onfrALTVD  33399  ax6e2ndeqVD  33417  ax6e2ndeqALT  33439  bnj1304  33585  rp-isfinite6  37409