Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alimdv | Unicode version |
Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 |
Ref | Expression |
---|---|
alimdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1519 | . 2 | |
2 | alimdv.1 | . 2 | |
3 | 1, 2 | alimdh 1460 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1440 ax-gen 1442 ax-17 1519 |
This theorem is referenced by: 2alimdv 1874 moim 2083 ralimdv2 2540 sstr2 3154 reuss2 3407 ssuni 3818 disjss2 3969 disjss1 3972 disjiun 3984 exmidsssnc 4189 soss 4299 alxfr 4446 ssrel 4699 ssrel2 4701 ssrelrel 4711 iotaval 5171 omnimkv 7132 |
Copyright terms: Public domain | W3C validator |