![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcn | GIF version |
Description: A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.) |
Ref | Expression |
---|---|
dcn | ⊢ (DECID 𝜑 → DECID ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 592 | . . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑) | |
2 | 1 | orim2i 711 | . . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
3 | 2 | orcoms 682 | . 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
4 | df-dc 777 | . 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) | |
5 | df-dc 777 | . 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑)) | |
6 | 3, 4, 5 | 3imtr4i 199 | 1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 662 DECID wdc 776 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 |
This theorem depends on definitions: df-bi 115 df-dc 777 |
This theorem is referenced by: pm5.18dc 811 pm4.67dc 815 pm2.54dc 824 imordc 830 pm4.54dc 839 stabtestimpdc 858 annimdc 879 pm4.55dc 880 orandc 881 pm3.12dc 900 pm3.13dc 901 dn1dc 902 xor3dc 1319 dfbi3dc 1329 dcned 2255 gcdaddm 10600 |
Copyright terms: Public domain | W3C validator |