Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dcbii | GIF version |
Description: Equivalence property for decidability. Inference form. (Contributed by Jim Kingdon, 28-Mar-2018.) |
Ref | Expression |
---|---|
dcbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
dcbii | ⊢ (DECID 𝜑 ↔ DECID 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dcbii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | dcbiit 834 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (DECID 𝜑 ↔ DECID 𝜓)) | |
3 | 1, 2 | ax-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 |