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 𝜑 → (𝜑 ∨ ¬ 𝜑))

Proof of Theorem exmiddc

Step	Hyp	Ref	Expression
1		df-dc 777	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2	1	biimpi 118	1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

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  1986  rabxmdc  3297  ifsbdc  3385  ifcldadc  3400  ifeq1dadc  3401  ifbothdadc  3402  ifbothdc  3403  eqifdc  3404  exmidundif  3999  dcextest  4359  dcdifsnid  6195  fidceq  6515  fidifsnen  6516  finexdc  6545  unfiexmid  6555  unsnfidcex  6557  unsnfidcel  6558  undifdcss  6560  ssfirab  6568  exmidomniim  6702  exmidfodomrlemim  6730  nnnninf  8645  exfzdc  9540  flqeqceilz  9614  modifeq2int  9682  modfzo0difsn  9691  modsumfzodifsn  9692  bcval  9992  bccmpl  9997  ibcval5  10006  bcpasc  10009  bccl  10010  hashfzp1  10067  sumdc  10569  isumrblem  10573  fisumcvg  10574  dvdsabseq  10628  zsupcllemstep  10721  infssuzex  10725  gcdval  10731  gcddvds  10735  gcdcl  10738  gcd0id  10750  gcdneg  10753  gcdaddm  10755  dfgcd3  10779  dfgcd2  10783  gcdmultiplez  10790  dvdssq  10800  dvdslcm  10831  lcmcl  10834  lcmneg  10836  lcmgcd  10840  lcmdvds  10841  lcmid  10842  mulgcddvds  10856  cncongr2  10866  prmind2  10882  rpexp  10912  pw2dvdslemn  10923  unennn  10990  sumdc2  11042  nnsf  11237  nninfsellemsuc  11246