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

Theorem dcbii 808
Description: Equivalence property for decidability. Inference form. (Contributed by Jim Kingdon, 28-Mar-2018.)
Hypothesis
Ref Expression
dcbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
dcbii  |-  (DECID  ph  <-> DECID  ps )

Proof of Theorem dcbii
StepHypRef Expression
1 dcbii.1 . 2  |-  ( ph  <->  ps )
2 dcbiit 807 . 2  |-  ( (
ph 
<->  ps )  ->  (DECID  ph  <-> DECID  ps ) )
31, 2ax-mp 5 1  |-  (DECID  ph  <-> DECID  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104  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:  dcbi  903  dcned  2289  dfrex2dc  2403  euxfr2dc  2840  exmidexmid  4088  exfzdc  9968  nninfsellemdc  13040
  Copyright terms: Public domain W3C validator