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 1505 | . 2 | |
2 | hbe1 1456 | . 2 | |
3 | 19.8a 1554 | . . . 4 | |
4 | 3 | imim2i 12 | . . 3 |
5 | 4 | sps 1502 | . 2 |
6 | 1, 2, 5 | exlimdh 1560 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1314 wex 1453 |
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-5 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eximi 1564 exbi 1568 eximdh 1575 19.29 1584 19.25 1590 alexim 1609 19.23t 1640 spimt 1699 equvini 1716 nfexd 1719 ax10oe 1753 sbcof2 1766 spsbim 1799 mor 2019 rexim 2503 elex22 2675 elex2 2676 vtoclegft 2732 spcimgft 2736 spcimegft 2738 spc2gv 2750 spc3gv 2752 ssoprab2 5795 bj-inf2vnlem1 13095 |
Copyright terms: Public domain | W3C validator |