![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alrimiv | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alrimiv.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
alrimiv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1416 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | alrimiv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | 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-5 1333 ax-gen 1335 ax-17 1416 |
This theorem is referenced by: alrimivv 1752 nfdv 1754 axext4 2021 eqrdv 2035 abbi2dv 2153 abbi1dv 2154 elex22 2563 elex2 2564 spcimdv 2631 spcimedv 2633 pm13.183 2675 sbcthdv 2772 sbcimdv 2817 ssrdv 2945 ss2abdv 3007 abssdv 3008 opprc 3561 dfnfc2 3589 intss 3627 intab 3635 dfiin2g 3681 disjss1 3742 mpteq12dva 3829 el 3922 euotd 3982 reusv1 4156 elirr 4224 sucprcreg 4227 en2lp 4232 tfisi 4253 ssrelrel 4383 issref 4650 iotaval 4821 iota5 4830 iotabidv 4831 funmo 4860 funco 4883 funun 4887 fununi 4910 funcnvuni 4911 funimaexglem 4925 fvssunirng 5133 relfvssunirn 5134 sefvex 5139 nfunsn 5150 f1oresrab 5272 funoprabg 5542 mpt2fvex 5771 1stconst 5784 2ndconst 5785 tfrexlem 5889 rdgexggg 5904 rdgifnon 5906 rdgifnon2 5907 rdgivallem 5908 frectfr 5924 frecrdg 5931 iserd 6068 pitonn 6744 frecuzrdgrrn 8875 frec2uzrdg 8876 frecuzrdgrom 8877 frecuzrdgfn 8879 frecuzrdgsuc 8882 2spim 9241 bj-om 9396 bj-nnord 9418 bj-inf2vn 9434 bj-inf2vn2 9435 bj-findis 9439 |
Copyright terms: Public domain | W3C validator |