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 591 | . . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑) | |
2 | 1 | orim2i 710 | . . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
3 | 2 | orcoms 681 | . 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
4 | df-dc 776 | . 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) | |
5 | df-dc 776 | . 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑)) | |
6 | 3, 4, 5 | 3imtr4i 199 | 1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 661 DECID wdc 775 |
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 576 ax-in2 577 ax-io 662 |
This theorem depends on definitions: df-bi 115 df-dc 776 |
This theorem is referenced by: pm5.18dc 810 pm4.67dc 814 pm2.54dc 823 imordc 829 pm4.54dc 838 stabtestimpdc 857 annimdc 878 pm4.55dc 879 orandc 880 pm3.12dc 899 pm3.13dc 900 dn1dc 901 xor3dc 1318 dfbi3dc 1328 dcned 2251 gcdaddm 10375 |
Copyright terms: Public domain | W3C validator |