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 3816 disjss2 3967 disjss1 3970 disjiun 3982 exmidsssnc 4187 soss 4297 alxfr 4444 ssrel 4697 ssrel2 4699 ssrelrel 4709 iotaval 5169 omnimkv 7130 |
Copyright terms: Public domain | W3C validator |