![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exim | Unicode version |
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
exim |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hba1 1479 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | hbe1 1430 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 19.8a 1528 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | imim2i 12 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | sps 1476 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | exlimdh 1533 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-ial 1473 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eximi 1537 exbi 1541 eximdh 1548 19.29 1557 19.25 1563 alexim 1582 19.23t 1613 spimt 1672 equvini 1689 nfexd 1692 ax10oe 1726 sbcof2 1739 spsbim 1772 mor 1991 rexim 2468 elex22 2635 elex2 2636 vtoclegft 2692 spcimgft 2696 spcimegft 2698 spc2gv 2710 spc3gv 2712 ssoprab2 5719 bj-inf2vnlem1 12138 |
Copyright terms: Public domain | W3C validator |