Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alrimih | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Ref | Expression |
---|---|
alrimih.1 | |
alrimih.2 |
Ref | Expression |
---|---|
alrimih |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimih.1 | . 2 | |
2 | alrimih.2 | . . 3 | |
3 | 2 | alimi 1448 | . 2 |
4 | 1, 3 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1440 ax-gen 1442 |
This theorem is referenced by: albidh 1473 alrimi 1515 nfd 1516 19.21h 1550 exlimd2 1588 exlimdh 1589 eximdh 1604 nexd 1606 exbidh 1607 hbex 1629 hbnd 1648 19.12 1658 19.38 1669 ax11i 1707 equsalh 1719 nfald 1753 nfexd 1754 aev 1805 equs5or 1823 sb4or 1826 sbbidh 1838 sb6rf 1846 alrimiv 1867 eupicka 2099 2moex 2105 |
Copyright terms: Public domain | W3C validator |