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

Theorem dcbii 835
Description: Equivalence property for decidability. Inference form. (Contributed by Jim Kingdon, 28-Mar-2018.)
Hypothesis
Ref Expression
dcbii.1 (𝜑𝜓)
Assertion
Ref Expression
dcbii (DECID 𝜑DECID 𝜓)

Proof of Theorem dcbii
StepHypRef Expression
1 dcbii.1 . 2 (𝜑𝜓)
2 dcbiit 834 . 2 ((𝜑𝜓) → (DECID 𝜑DECID 𝜓))
31, 2ax-mp 5 1 (DECID 𝜑DECID 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  DECID wdc 829
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 609  ax-in2 610  ax-io 704
This theorem depends on definitions:  df-bi 116  df-dc 830
This theorem is referenced by:  dcbi  931  dcned  2346  dfrex2dc  2461  euxfr2dc  2915  exmidexmid  4182  pw1fin  6888  dcfi  6958  elnn0dc  9570  elnndc  9571  exfzdc  10196  fprod1p  11562  nnwosdc  11994  prmdc  12084  pclemdc  12242  nninfdclemcl  12403  nninfdclemp1  12405  nninfsellemdc  14043
  Copyright terms: Public domain W3C validator