![]() |
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 1467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | alrimi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | alrimih 1413 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-5 1391 ax-gen 1393 ax-4 1455 |
This theorem depends on definitions: df-bi 116 df-nf 1405 |
This theorem is referenced by: 19.32r 1626 cbv3 1688 sbbid 1785 sbalyz 1935 dvelimdf 1952 dvelimor 1954 abbid 2216 nfcd 2235 ralrimi 2462 r19.32r 2536 ceqsalg 2669 ceqsex 2679 vtocldf 2692 elrab3t 2792 morex 2821 sbciedf 2896 csbiebt 2989 csbiedf 2990 ssrd 3052 rgenm 3412 invdisj 3869 ssopab2b 4136 eusv2nf 4315 sniota 5051 imadif 5139 funimaexglem 5142 eusvobj1 5693 ssoprab2b 5760 ovmpodxf 5828 |
Copyright terms: Public domain | W3C validator |