![]() |
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 627 | . . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
3 | 1, 2 | orbi12d 742 | . 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒))) |
4 | df-dc 781 | . 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓)) | |
5 | df-dc 781 | . 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 664 DECID wdc 780 |
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 579 ax-in2 580 ax-io 665 |
This theorem depends on definitions: df-bi 115 df-dc 781 |
This theorem is referenced by: exmidexmid 4031 exmidel 4034 dcdifsnid 6263 finexdc 6616 undifdcss 6631 ssfirab 6641 fidcenumlemrks 6660 ltdcpi 6880 enqdc 6918 enqdc1 6919 ltdcnq 6954 fzodcel 9559 exfzdc 9647 sumeq1 10740 sumdc 10743 isummolem2 10768 isummo 10769 zisum 10770 fisum 10774 isumz 10777 isumss 10779 fisumss 10780 isumss2 10781 fisumcvg2 10782 fsum3cvg2 10783 fisumsers 10784 fsumsplit 10797 dvdsdc 11078 zdvdsdc 11091 zsupcllemstep 11215 infssuzex 11219 hashdvds 11471 sumdc2 11654 nninfsellemdc 11857 |
Copyright terms: Public domain | W3C validator |