Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-stdc Unicode version

Theorem bj-stdc 14739
Description: Decidability of a proposition is stable if and only if that proposition is decidable. In particular, the assumption that every formula is stable implies that every formula is decidable, hence classical logic. (Contributed by BJ, 9-Oct-2019.)
Assertion
Ref Expression
bj-stdc  |-  (STAB DECID  ph  <-> DECID  ph )

Proof of Theorem bj-stdc
StepHypRef Expression
1 nndc 852 . 2  |-  -.  -. DECID  ph
2 bj-nnbist 14723 . 2  |-  ( -. 
-. DECID  ph  ->  (STAB DECID  ph  <-> DECID  ph )
)
31, 2ax-mp 5 1  |-  (STAB DECID  ph  <-> DECID  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 105  STAB wstab 831  DECID wdc 835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator