![]() |
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 1847 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | alrimiv 1847 |
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-5 1424 ax-gen 1426 ax-17 1507 |
This theorem is referenced by: 2ax17 1851 euind 2875 sbnfc2 3065 exmidsssn 4133 exmidel 4136 exmidundif 4137 exmidundifim 4138 ssopab2dv 4208 suctr 4351 eusvnf 4382 ordsuc 4486 ssrel 4635 relssdv 4639 eqrelrdv 4643 eqbrrdv 4644 eqrelrdv2 4646 ssrelrel 4647 iss 4873 funssres 5173 funun 5175 fununi 5199 fsn 5600 ovg 5917 caovimo 5972 oprabexd 6033 qliftfund 6520 eroveu 6528 th3qlem1 6539 exmidfodomrlemim 7074 addnq0mo 7279 mulnq0mo 7280 ltexprlemdisj 7438 recexprlemdisj 7462 addsrmo 7575 mulsrmo 7576 summodc 11184 prodmodc 11379 limcimo 12842 exmidsbth 13394 |
Copyright terms: Public domain | W3C validator |