Theorem exmid 405

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. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
exmid	|- ( ph \/ -. ph )

Proof of Theorem exmid

Step	Hyp	Ref	Expression
1		id 20	. 2 |- ( -. ph -> -. ph )
2	1	orri 366	1 |- ( ph \/ -. ph )

Syntax hints:   -. wn 3   \/ wo 358

This theorem is referenced by:  exmidd  406  pm5.62  890  pm5.63  891  pm4.83  896  4exmid  906  jaoi2  934  exmidne  2573  elimif  3728  xpima  5272  ixxun  10888  lgsquadlem2  21092  cusgrasizeindslem2  21436  ifbieq12d2  23955  elimifd  23957  elim2if  23958  elim2ifim  23959  iocinif  24097  hasheuni  24428  voliune  24538  volfiniune  24539  fvresval  25337  cnambfre  26154  uunT1  28601  onfrALTVD  28712  a9e2ndeqVD  28730  a9e2ndeqALT  28753  bnj1304  28897

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-or 360