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

Theorem dcn 810
Description: The negation of a decidable proposition is decidable. The converse need not hold, but does hold for negated propositions, see dcnn 816. (Contributed by Jim Kingdon, 25-Mar-2018.)
Assertion
Ref Expression
dcn  |-  (DECID  ph  -> DECID  -.  ph )

Proof of Theorem dcn
StepHypRef Expression
1 notnot 601 . . . 4  |-  ( ph  ->  -.  -.  ph )
21orim2i 733 . . 3  |-  ( ( -.  ph  \/  ph )  ->  ( -.  ph  \/  -.  -.  ph ) )
32orcoms 702 . 2  |-  ( (
ph  \/  -.  ph )  ->  ( -.  ph  \/  -.  -.  ph ) )
4 df-dc 803 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
5 df-dc 803 . 2  |-  (DECID  -.  ph  <->  ( -.  ph  \/  -.  -.  ph ) )
63, 4, 53imtr4i 200 1  |-  (DECID  ph  -> DECID  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 680  DECID wdc 802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681
This theorem depends on definitions:  df-bi 116  df-dc 803
This theorem is referenced by:  stdcndc  813  stdcndcOLD  814  dcnn  816  pm5.18dc  851  pm4.67dc  855  pm2.54dc  859  imordc  865  pm4.54dc  870  annimdc  904  pm4.55dc  905  orandc  906  pm3.12dc  925  pm3.13dc  926  dn1dc  927  xor3dc  1348  dfbi3dc  1358  dcned  2289  gcdaddm  11579
  Copyright terms: Public domain W3C validator