![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcbid | Unicode version |
Description: The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.) |
Ref | Expression |
---|---|
dcbid.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
dcbid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dcbid.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | notbid 628 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 1, 2 | orbi12d 743 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-dc 782 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-dc 782 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3bitr4g 222 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 ax-io 666 |
This theorem depends on definitions: df-bi 116 df-dc 782 |
This theorem is referenced by: exmidexmid 4039 exmidel 4044 dcdifsnid 6279 finexdc 6674 undifdcss 6689 ssfirab 6699 fidcenumlemrks 6718 ltdcpi 6945 enqdc 6983 enqdc1 6984 ltdcnq 7019 fzodcel 9626 exfzdc 9714 sumeq1 10807 sumdc 10810 isummolem2 10835 isummo 10836 zisum 10837 fisum 10841 isumz 10844 isumss 10846 fisumss 10847 isumss2 10848 fisumcvg2 10849 fsum3cvg2 10850 fisumsers 10851 fsumsplit 10864 dvdsdc 11145 zdvdsdc 11158 zsupcllemstep 11282 infssuzex 11286 hashdvds 11538 sumdc2 12003 nninfsellemdc 12205 |
Copyright terms: Public domain | W3C validator |