![]() |
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 1409 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | alrimi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | alrimih 1355 |
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 99 ax-5 1333 ax-gen 1335 ax-4 1397 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: 19.32r 1567 cbv3 1627 sbalyz 1872 dvelimdf 1889 dvelimor 1891 abbid 2151 nfcd 2170 ralrimi 2384 r19.32r 2451 ceqsalg 2576 ceqsex 2586 vtocldf 2599 elrab3t 2691 morex 2719 sbciedf 2792 csbiebt 2880 csbiedf 2881 ssrd 2944 rgenm 3317 invdisj 3750 ssopab2b 4004 eusv2nf 4154 sniota 4837 imadif 4922 funimaexglem 4925 eusvobj1 5442 ssoprab2b 5504 ovmpt2dxf 5568 |
Copyright terms: Public domain | W3C validator |