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

Theorem dcn 784
Description: A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.)
Assertion
Ref Expression
dcn  |-  (DECID  ph  -> DECID  -.  ph )

Proof of Theorem dcn
StepHypRef Expression
1 notnot 594 . . . 4  |-  ( ph  ->  -.  -.  ph )
21orim2i 713 . . 3  |-  ( ( -.  ph  \/  ph )  ->  ( -.  ph  \/  -.  -.  ph ) )
32orcoms 684 . 2  |-  ( (
ph  \/  -.  ph )  ->  ( -.  ph  \/  -.  -.  ph ) )
4 df-dc 781 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
5 df-dc 781 . 2  |-  (DECID  -.  ph  <->  ( -.  ph  \/  -.  -.  ph ) )
63, 4, 53imtr4i 199 1  |-  (DECID  ph  -> DECID  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 664  DECID wdc 780
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665
This theorem depends on definitions:  df-bi 115  df-dc 781
This theorem is referenced by:  pm5.18dc  815  pm4.67dc  819  pm2.54dc  828  imordc  834  pm4.54dc  843  stabtestimpdc  862  annimdc  883  pm4.55dc  884  orandc  885  pm3.12dc  904  pm3.13dc  905  dn1dc  906  xor3dc  1323  dfbi3dc  1333  dcned  2261  gcdaddm  11249
  Copyright terms: Public domain W3C validator