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 23	. 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  932  pm5.63  933  pm4.83  938  4exmid  948  cases  980  exmidneOLD  2631  xpima  5296  ixxun  11653  trclfvg  13073  lgsquadlem2  24275  cusgrasizeindslem2  25194  ifbieq12d2  28155  elimifd  28156  elim2ifim  28158  iocinif  28363  hasheuni  28908  voliune  29054  volfiniune  29055  bnj1304  29633  fvresval  30409  wl-cases2-dnf  31808  cnambfre  31947  tsim1  32330  rp-isfinite6  36127  uunT1  37072  onfrALTVD  37193  ax6e2ndeqVD  37211  ax6e2ndeqALT  37233  testable  39883