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 1506 | . 2 |
3 | alrimi.2 | . 2 | |
4 | 2, 3 | alrimih 1456 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1340 wnf 1447 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-5 1434 ax-gen 1436 ax-4 1497 |
This theorem depends on definitions: df-bi 116 df-nf 1448 |
This theorem is referenced by: axc4i 1529 19.32r 1667 cbv3 1729 sbbid 1833 sbalyz 1986 dvelimdf 2003 dvelimor 2005 nf5d 2012 abbid 2281 nfcd 2301 nfabdw 2325 ralrimi 2535 r19.32r 2610 ceqsalg 2749 ceqsex 2759 vtocldf 2772 elrab3t 2876 morex 2905 sbciedf 2981 csbiebt 3079 csbiedf 3080 ssrd 3142 rgenm 3506 invdisj 3970 ssopab2b 4248 eusv2nf 4428 sniota 5174 imadif 5262 funimaexglem 5265 eusvobj1 5823 ssoprab2b 5890 ovmpodxf 5958 |
Copyright terms: Public domain | W3C validator |