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 1491 | . 2 | |
2 | 1 | 19.41h 1648 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wex 1453 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.41vv 1859 19.41vvv 1860 19.41vvvv 1861 exdistrv 1864 eeeanv 1885 gencbvex 2706 euxfrdc 2843 euind 2844 dfdif3 3156 r19.9rmv 3424 opabm 4172 eliunxp 4648 relop 4659 dmuni 4719 dmres 4810 dminss 4923 imainss 4924 ssrnres 4951 cnvresima 4998 resco 5013 rnco 5015 coass 5027 xpcom 5055 f11o 5368 fvelrnb 5437 rnoprab 5822 domen 6613 xpassen 6692 genpassl 7300 genpassu 7301 |
Copyright terms: Public domain | W3C validator |