Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alrimivv | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 |
Ref | Expression |
---|---|
alrimivv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 | |
2 | 1 | alrimiv 1795 | . 2 |
3 | 2 | alrimiv 1795 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1282 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-5 1376 ax-gen 1378 ax-17 1459 |
This theorem is referenced by: 2ax17 1799 euind 2779 sbnfc2 2962 ssopab2dv 4033 suctr 4176 eusvnf 4203 ordsuc 4306 ssrel 4446 relssdv 4450 eqrelrdv 4454 eqbrrdv 4455 eqrelrdv2 4457 ssrelrel 4458 iss 4674 funssres 4962 funun 4964 fununi 4987 fsn 5356 ovg 5659 caovimo 5714 oprabexd 5774 qliftfund 6212 eroveu 6220 th3qlem1 6231 addnq0mo 6637 mulnq0mo 6638 ltexprlemdisj 6796 recexprlemdisj 6820 addsrmo 6920 mulsrmo 6921 |
Copyright terms: Public domain | W3C validator |