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 1435 | . 2 |
4 | 1, 3 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1333 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1427 ax-gen 1429 |
This theorem is referenced by: albidh 1460 alrimi 1502 nfd 1503 19.21h 1537 exlimd2 1575 exlimdh 1576 eximdh 1591 nexd 1593 exbidh 1594 hbex 1616 hbnd 1635 19.12 1645 19.38 1656 ax11i 1694 equsalh 1706 nfald 1740 nfexd 1741 aev 1792 equs5or 1810 sb4or 1813 sbbidh 1825 sb6rf 1833 alrimiv 1854 eupicka 2086 2moex 2092 |
Copyright terms: Public domain | W3C validator |