Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alrimi | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
alrimi.1 | |
alrimi.2 |
Ref | Expression |
---|---|
alrimi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimi.1 | . . 3 | |
2 | 1 | nfri 1412 | . 2 |
3 | alrimi.2 | . 2 | |
4 | 2, 3 | alrimih 1358 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1241 wnf 1349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-5 1336 ax-gen 1338 ax-4 1400 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: 19.32r 1570 cbv3 1630 sbalyz 1875 dvelimdf 1892 dvelimor 1894 abbid 2154 nfcd 2173 ralrimi 2390 r19.32r 2457 ceqsalg 2582 ceqsex 2592 vtocldf 2605 elrab3t 2697 morex 2725 sbciedf 2798 csbiebt 2886 csbiedf 2887 ssrd 2950 rgenm 3323 invdisj 3759 ssopab2b 4013 eusv2nf 4188 sniota 4894 imadif 4979 funimaexglem 4982 eusvobj1 5499 ssoprab2b 5562 ovmpt2dxf 5626 |
Copyright terms: Public domain | W3C validator |