![]() |
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 1530 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | alrimi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | alrimih 1480 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-5 1458 ax-gen 1460 ax-4 1521 |
This theorem depends on definitions: df-bi 117 df-nf 1472 |
This theorem is referenced by: axc4i 1553 19.32r 1691 cbv3 1753 sbbid 1857 sbalyz 2011 dvelimdf 2028 dvelimor 2030 nf5d 2037 abbid 2306 nfcd 2327 nfabdw 2351 ralrimi 2561 r19.32r 2636 ceqsalg 2780 ceqsex 2790 vtocldf 2803 elrab3t 2907 morex 2936 sbciedf 3013 csbiebt 3111 csbiedf 3112 ssrd 3175 rgenm 3540 invdisj 4012 ssopab2b 4294 eusv2nf 4474 sniota 5226 imadif 5315 funimaexglem 5318 eusvobj1 5883 ssoprab2b 5953 ovmpodxf 6022 |
Copyright terms: Public domain | W3C validator |