ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmiddc Unicode version

Theorem exmiddc 778
Description: Law of excluded middle, for a decidable proposition. The law of the excluded middle is 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. The key way in which intuitionistic logic differs from classical logic is that intuitionistic logic says that excluded middle only holds for some propositions, and classical logic says that it holds for all propositions. (Contributed by Jim Kingdon, 12-May-2018.)
Assertion
Ref Expression
exmiddc  |-  (DECID  ph  ->  (
ph  \/  -.  ph )
)

Proof of Theorem exmiddc
StepHypRef Expression
1 df-dc 777 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
21biimpi 118 1  |-  (DECID  ph  ->  (
ph  \/  -.  ph )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 662  DECID wdc 776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-dc 777
This theorem is referenced by:  stabtestimpdc  858  modc  1985  rabxmdc  3283  ifsbdc  3371  ifcldadc  3386  ifeq1dadc  3387  ifbothdc  3388  fidceq  6404  fidifsnen  6405  unfiexmid  6438  unsnfidcex  6440  unsnfidcel  6441  exfzdc  9326  flqeqceilz  9400  modifeq2int  9468  modfzo0difsn  9477  modsumfzodifsn  9478  bcval  9773  bccmpl  9778  ibcval5  9787  bcpasc  9790  bccl  9791  sumdc  10333  isumrblem  10337  fisumcvg  10338  dvdsabseq  10392  zsupcllemstep  10485  infssuzex  10489  gcdval  10495  gcddvds  10499  gcdcl  10502  gcd0id  10514  gcdneg  10517  gcdaddm  10519  dfgcd3  10543  dfgcd2  10547  gcdmultiplez  10554  dvdssq  10564  dvdslcm  10595  lcmcl  10598  lcmneg  10600  lcmgcd  10604  lcmdvds  10605  lcmid  10606  mulgcddvds  10620  cncongr2  10630  prmind2  10646  rpexp  10676  pw2dvdslemn  10687  unennn  10708  sumdc2  10760
  Copyright terms: Public domain W3C validator