Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dcbid | Unicode version |
Description: Equivalence property for decidability. Deduction form. (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 657 | . . 3 |
3 | 1, 2 | orbi12d 783 | . 2 |
4 | df-dc 821 | . 2 DECID | |
5 | df-dc 821 | . 2 DECID | |
6 | 3, 4, 5 | 3bitr4g 222 | 1 DECID DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 104 wo 698 DECID wdc 820 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 |
This theorem depends on definitions: df-bi 116 df-dc 821 |
This theorem is referenced by: dcbiit 825 exmidexmid 4157 exmidel 4166 dcdifsnid 6451 finexdc 6847 pw1dc1 6858 undifdcss 6867 ssfirab 6878 fidcenumlemrks 6897 dcfi 6925 difinfsnlem 7043 difinfsn 7044 ctssdclemn0 7054 ctssdccl 7055 ctssdclemr 7056 ctssdc 7057 iswomni 7108 enwomnilem 7112 ltdcpi 7243 enqdc 7281 enqdc1 7282 ltdcnq 7317 fzodcel 10051 exfzdc 10139 sumeq1 11252 sumdc 11255 summodclem2 11279 summodc 11280 zsumdc 11281 fsum3 11284 isumz 11286 isumss 11288 fisumss 11289 isumss2 11290 fsum3cvg2 11291 fsumsersdc 11292 fsumsplit 11304 prodeq1f 11449 prodmodclem2a 11473 prodmodclem2 11474 prodmodc 11475 zproddc 11476 fprodseq 11480 prod1dc 11483 prodssdc 11486 fprodssdc 11487 fprodsplitdc 11493 dvdsdc 11694 zdvdsdc 11707 zsupcllemstep 11831 infssuzex 11835 nninfdcex 11838 hashdvds 12095 eulerthlemfi 12102 phisum 12114 ennnfonelemr 12152 ennnfonelemim 12153 ctinf 12159 ctiunctlemudc 12166 ctiunct 12169 ssomct 12174 ssnnctlemct 12175 nnmindc 12177 nnminle 12178 nninfdclemcl 12179 nninfdclemp1 12181 sumdc2 13373 bj-charfundcALT 13384 bj-charfunbi 13386 nninfsellemdc 13582 iswomninnlem 13620 iswomni0 13622 redcwlpo 13626 redc0 13628 reap0 13629 dceqnconst 13630 dcapnconst 13631 |
Copyright terms: Public domain | W3C validator |