![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dtru | Unicode version |
Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). If we assumed the law of the excluded middle this would be equivalent to dtruex 4512. (Contributed by Jim Kingdon, 29-Dec-2018.) |
Ref | Expression |
---|---|
dtru |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dtruex 4512 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | exnalim 1623 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-pow 4130 ax-setind 4490 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-ral 2437 df-v 2711 df-dif 3100 df-in 3104 df-ss 3111 df-pw 3541 df-sn 3562 |
This theorem is referenced by: oprabidlem 5842 |
Copyright terms: Public domain | W3C validator |