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 1512 | . 2 |
3 | alrimi.2 | . 2 | |
4 | 2, 3 | alrimih 1462 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1346 wnf 1453 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-5 1440 ax-gen 1442 ax-4 1503 |
This theorem depends on definitions: df-bi 116 df-nf 1454 |
This theorem is referenced by: axc4i 1535 19.32r 1673 cbv3 1735 sbbid 1839 sbalyz 1992 dvelimdf 2009 dvelimor 2011 nf5d 2018 abbid 2287 nfcd 2307 nfabdw 2331 ralrimi 2541 r19.32r 2616 ceqsalg 2758 ceqsex 2768 vtocldf 2781 elrab3t 2885 morex 2914 sbciedf 2990 csbiebt 3088 csbiedf 3089 ssrd 3152 rgenm 3516 invdisj 3981 ssopab2b 4259 eusv2nf 4439 sniota 5187 imadif 5276 funimaexglem 5279 eusvobj1 5837 ssoprab2b 5907 ovmpodxf 5975 |
Copyright terms: Public domain | W3C validator |