Theorem exmiddc 785

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 667  DECID wdc 783

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-dc 784

This theorem is referenced by:  stabtestimpdc  865  modc  1998  rabxmdc  3333  dcun  3412  ifsbdc  3425  ifcldadc  3440  ifeq1dadc  3441  ifbothdadc  3442  ifbothdc  3443  ifiddc  3444  eqifdc  3445  exmidn0m  4054  exmidundif  4058  exmidundifim  4059  dcextest  4424  dcdifsnid  6303  fidceq  6665  fidifsnen  6666  fimax2gtrilemstep  6696  finexdc  6698  unfiexmid  6708  unsnfidcex  6710  unsnfidcel  6711  undifdcss  6713  ssfirab  6723  fidcenumlemrks  6742  exmidomniim  6884  nnnninf  6894  exmidfodomrlemim  6924  xaddcom  9427  xnegdi  9434  xpncan  9437  xleadd1a  9439  xsubge0  9447  exfzdc  9800  flqeqceilz  9874  modifeq2int  9942  modfzo0difsn  9951  modsumfzodifsn  9952  iseqf1olemab  10039  iseqf1olemmo  10042  seq3f1olemstep  10051  fser0const  10066  bcval  10272  bccmpl  10277  bcval5  10286  bcpasc  10289  bccl  10290  hashfzp1  10347  2zsupmax  10772  xrmaxifle  10789  xrmaxiflemab  10790  xrmaxiflemlub  10791  xrmaxiflemcom  10792  sumdc  10901  sumrbdclem  10919  fsum3cvg  10920  summodclem2a  10924  zsumdc  10927  isumss  10934  fisumss  10935  isumss2  10936  fsumadd  10949  sumsplitdc  10975  fsummulc2  10991  dvdsabseq  11275  zsupcllemstep  11368  infssuzex  11372  gcdval  11378  gcddvds  11382  gcdcl  11385  gcd0id  11397  gcdneg  11400  gcdaddm  11402  dfgcd3  11426  dfgcd2  11430  gcdmultiplez  11437  dvdssq  11447  dvdslcm  11478  lcmcl  11481  lcmneg  11483  lcmgcd  11487  lcmdvds  11488  lcmid  11489  mulgcddvds  11503  cncongr2  11513  prmind2  11529  rpexp  11559  pw2dvdslemn  11570  unennn  11637  sumdc2  12407  nnsf  12600  nninfsellemsuc  12609