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  jaoi2OLD  967  cases  969  cases2OLD  971  exmidneOLD  2673  xpima  5455  ixxun  11557  lgsquadlem2  23496  cusgrasizeindslem2  24297  ifbieq12d2  27243  elimifd  27244  elim2if  27245  elim2ifim  27246  iocinif  27415  hasheuni  27916  voliune  28026  volfiniune  28027  fvresval  29124  cnambfre  29990  tsim1  30465  testable  32697  uunT1  33058  onfrALTVD  33172  ax6e2ndeqVD  33190  ax6e2ndeqALT  33212  bnj1304  33358