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 1419 | . 2 | |
2 | 1 | 19.41h 1575 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wb 98 wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 19.41vv 1783 19.41vvv 1784 19.41vvvv 1785 eeeanv 1808 gencbvex 2600 euxfrdc 2727 euind 2728 r19.9rmv 3313 opabm 4017 eliunxp 4475 relop 4486 dmuni 4545 dmres 4632 dminss 4738 imainss 4739 ssrnres 4763 cnvresima 4810 resco 4825 rnco 4827 coass 4839 xpcom 4864 f11o 5159 fvelrnb 5221 rnoprab 5587 domen 6232 xpassen 6304 genpassl 6622 genpassu 6623 |
Copyright terms: Public domain | W3C validator |