Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dcne | Unicode version |
Description: Decidable equality expressed in terms of . Basically the same as df-dc 830. (Contributed by Jim Kingdon, 14-Mar-2020.) |
Ref | Expression |
---|---|
dcne | DECID |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dc 830 | . 2 DECID | |
2 | df-ne 2341 | . . 3 | |
3 | 2 | orbi2i 757 | . 2 |
4 | 1, 3 | bitr4i 186 | 1 DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wb 104 wo 703 DECID wdc 829 wceq 1348 wne 2340 |
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-io 704 |
This theorem depends on definitions: df-bi 116 df-dc 830 df-ne 2341 |
This theorem is referenced by: updjudhf 7056 zdceq 9287 nn0lt2 9293 xlesubadd 9840 qdceq 10203 xrmaxadd 11224 nn0seqcvgd 11995 pcxnn0cl 12264 pcge0 12266 pcdvdsb 12273 pcneg 12278 pcdvdstr 12280 pcgcd1 12281 pc2dvds 12283 pcz 12285 pcprmpw2 12286 pcaddlem 12292 pcadd 12293 pcmpt 12295 qexpz 12304 lgsneg1 13720 lgsdirprm 13729 lgsdir 13730 lgsne0 13733 lgsdirnn0 13742 lgsdinn0 13743 2sqlem9 13754 tridceq 14088 |
Copyright terms: Public domain | W3C validator |