![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcne | Unicode version |
Description: Decidable equality
expressed in terms of ![]() |
Ref | Expression |
---|---|
dcne |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dc 836 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-ne 2361 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | orbi2i 763 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitr4i 187 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
This theorem depends on definitions: df-bi 117 df-dc 836 df-ne 2361 |
This theorem is referenced by: updjudhf 7108 zdceq 9358 nn0lt2 9364 xlesubadd 9913 qdceq 10277 xrmaxadd 11301 nn0seqcvgd 12073 pcxnn0cl 12342 pcxqcl 12344 pcge0 12345 pcdvdsb 12352 pcneg 12357 pcdvdstr 12359 pcgcd1 12360 pc2dvds 12362 pcz 12364 pcprmpw2 12365 pcaddlem 12371 pcadd 12372 pcmpt 12375 qexpz 12384 4sqlem19 12441 lgsneg1 14887 lgsdirprm 14896 lgsdir 14897 lgsne0 14900 lgsdirnn0 14909 lgsdinn0 14910 2sqlem9 14932 tridceq 15266 |
Copyright terms: Public domain | W3C validator |