Theorem exmiddc 777

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 776	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2	1	biimpi 118	1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 661  DECID wdc 775

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 776

This theorem is referenced by:  stabtestimpdc  857  modc  1984  rabxmdc  3276  ifsbdc  3363  ifcldadc  3378  ifeq1dadc  3379  ifbothdc  3380  fidceq  6354  fidifsnen  6355  unsnfidcex  6385  unsnfidcel  6386  exfzdc  9249  flqeqceilz  9320  modifeq2int  9388  modfzo0difsn  9397  modsumfzodifsn  9398  bcval  9676  bccmpl  9681  ibcval5  9690  bcpasc  9693  bccl  9694  dvdsabseq  10247  zsupcllemstep  10341  infssuzex  10345  gcdval  10351  gcddvds  10355  gcdcl  10358  gcd0id  10370  gcdneg  10373  gcdaddm  10375  dfgcd3  10399  dfgcd2  10403  gcdmultiplez  10410  dvdssq  10420  dvdslcm  10451  lcmcl  10454  lcmneg  10456  lcmgcd  10460  lcmdvds  10461  lcmid  10462  mulgcddvds  10476  cncongr2  10486  prmind2  10502  rpexp  10532  pw2dvdslemn  10543