![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcbid | GIF version |
Description: The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.) |
Ref | Expression |
---|---|
dcbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
dcbid | ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dcbid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | notbid 625 | . . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
3 | 1, 2 | orbi12d 740 | . 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒))) |
4 | df-dc 777 | . 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓)) | |
5 | df-dc 777 | . 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒)) | |
6 | 3, 4, 5 | 3bitr4g 221 | 1 ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 103 ∨ 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: exmidexmid 3995 exmidel 3998 dcdifsnid 6195 finexdc 6545 undifdcss 6560 ssfirab 6568 ltdcpi 6785 enqdc 6823 enqdc1 6824 ltdcnq 6859 exfzdc 9540 sumeq1 10566 sumdc 10569 dvdsdc 10584 zdvdsdc 10597 zsupcllemstep 10721 infssuzex 10725 hashdvds 10977 sumdc2 11042 |
Copyright terms: Public domain | W3C validator |