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 641 | . . 3 |
3 | 1, 2 | orbi12d 767 | . 2 |
4 | df-dc 805 | . 2 DECID | |
5 | df-dc 805 | . 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 682 DECID wdc 804 |
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 588 ax-in2 589 ax-io 683 |
This theorem depends on definitions: df-bi 116 df-dc 805 |
This theorem is referenced by: dcbiit 809 exmidexmid 4090 exmidel 4098 dcdifsnid 6368 finexdc 6764 undifdcss 6779 ssfirab 6790 fidcenumlemrks 6809 difinfsnlem 6952 difinfsn 6953 ctssdclemn0 6963 ctssdccl 6964 ctssdclemr 6965 ctssdc 6966 ltdcpi 7099 enqdc 7137 enqdc1 7138 ltdcnq 7173 fzodcel 9884 exfzdc 9972 sumeq1 11079 sumdc 11082 summodclem2 11106 summodc 11107 zsumdc 11108 fsum3 11111 isumz 11113 isumss 11115 fisumss 11116 isumss2 11117 fsum3cvg2 11118 fsumsersdc 11119 fsumsplit 11131 dvdsdc 11413 zdvdsdc 11426 zsupcllemstep 11550 infssuzex 11554 hashdvds 11808 ennnfonelemr 11847 ennnfonelemim 11848 ctinf 11854 ctiunctlemudc 11861 ctiunct 11864 sumdc2 12902 nninfsellemdc 13102 |
Copyright terms: Public domain | W3C validator |