Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 19.41v | Unicode version |
Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.41v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1506 | . 2 | |
2 | 1 | 19.41h 1665 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wex 1472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.41vv 1883 19.41vvv 1884 19.41vvvv 1885 exdistrv 1890 eeeanv 1913 gencbvex 2758 euxfrdc 2898 euind 2899 dfdif3 3218 r19.9rmv 3486 opabm 4242 eliunxp 4727 relop 4738 dmuni 4798 dmres 4889 dminss 5002 imainss 5003 ssrnres 5030 cnvresima 5077 resco 5092 rnco 5094 coass 5106 xpcom 5134 f11o 5449 fvelrnb 5518 rnoprab 5906 domen 6698 xpassen 6777 genpassl 7446 genpassu 7447 |
Copyright terms: Public domain | W3C validator |