Theorem exmiddc 804

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

Step	Hyp	Ref	Expression
1		df-dc 803	. 2 |- (DECID ph <-> ( ph \/ -. ph ) )
2	1	biimpi 119	1 |- (DECID ph -> ( ph \/ -. ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 680  DECID wdc 802

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 803

This theorem is referenced by:  stdcndcOLD  814  modc  2018  rabxmdc  3360  dcun  3439  ifsbdc  3452  ifcldadc  3467  ifeq1dadc  3468  ifbothdadc  3469  ifbothdc  3470  ifiddc  3471  eqifdc  3472  exmid1dc  4083  exmidn0m  4084  exmidundif  4089  exmidundifim  4090  dcextest  4455  dcdifsnid  6354  fidceq  6716  fidifsnen  6717  fimax2gtrilemstep  6747  finexdc  6749  unfiexmid  6759  unsnfidcex  6761  unsnfidcel  6762  undifdcss  6764  ssfirab  6774  fidcenumlemrks  6793  omp1eomlem  6931  difinfsnlem  6936  difinfsn  6937  ctssdc  6950  exmidomniim  6963  nnnninf  6973  exmidfodomrlemim  7005  xaddcom  9537  xnegdi  9544  xpncan  9547  xleadd1a  9549  xsubge0  9557  exfzdc  9910  flqeqceilz  9984  modifeq2int  10052  modfzo0difsn  10061  modsumfzodifsn  10062  iseqf1olemab  10155  iseqf1olemmo  10158  seq3f1olemstep  10167  fser0const  10182  bcval  10388  bccmpl  10393  bcval5  10402  bcpasc  10405  bccl  10406  hashfzp1  10463  2zsupmax  10889  xrmaxifle  10907  xrmaxiflemab  10908  xrmaxiflemlub  10909  xrmaxiflemcom  10910  sumdc  11019  sumrbdclem  11037  fsum3cvg  11038  summodclem2a  11042  zsumdc  11045  isumss  11052  fisumss  11053  isumss2  11054  fsumadd  11067  sumsplitdc  11093  fsummulc2  11109  dvdsabseq  11393  zsupcllemstep  11486  infssuzex  11490  gcdval  11496  gcddvds  11500  gcdcl  11503  gcd0id  11515  gcdneg  11518  gcdaddm  11520  dfgcd3  11544  dfgcd2  11548  gcdmultiplez  11555  dvdssq  11565  dvdslcm  11596  lcmcl  11599  lcmneg  11601  lcmgcd  11605  lcmdvds  11606  lcmid  11607  mulgcddvds  11621  cncongr2  11631  prmind2  11647  rpexp  11677  pw2dvdslemn  11688  unennn  11755  ennnfonelemss  11768  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ctiunctlemudc  11793  sumdc2  12698  nnsf  12891  nninfsellemsuc  12900  nninffeq  12908