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

Theorem dcbii 840
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 839 . 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 105  DECID wdc 834
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 614  ax-in2 615  ax-io 709
This theorem depends on definitions:  df-bi 117  df-dc 835
This theorem is referenced by:  dcbi  936  dcned  2353  dfrex2dc  2468  euxfr2dc  2922  exmidexmid  4196  pw1fin  6909  dcfi  6979  elnn0dc  9609  elnndc  9610  exfzdc  10237  fprod1p  11602  nnwosdc  12034  prmdc  12124  pclemdc  12282  nninfdclemcl  12443  nninfdclemp1  12445  nninfsellemdc  14679
  Copyright terms: Public domain W3C validator