Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exlimdvv | Unicode version |
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
exlimdvv.1 |
Ref | Expression |
---|---|
exlimdvv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimdvv.1 | . . 3 | |
2 | 1 | exlimdv 1791 | . 2 |
3 | 2 | exlimdv 1791 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-5 1423 ax-gen 1425 ax-ie2 1470 ax-17 1506 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: euotd 4171 funopg 5152 th3qlem1 6524 fundmen 6693 sbthlemi10 6847 addnq0mo 7248 mulnq0mo 7249 genprndl 7322 genprndu 7323 genpdisj 7324 mullocpr 7372 addsrmo 7544 mulsrmo 7545 cnm 7633 summodc 11145 fsum2dlemstep 11196 txbasval 12425 |
Copyright terms: Public domain | W3C validator |