![]() |
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 1464 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 19.41h 1620 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-17 1464 ax-ial 1472 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 19.41vv 1831 19.41vvv 1832 19.41vvvv 1833 eeeanv 1856 gencbvex 2665 euxfrdc 2801 euind 2802 dfdif3 3110 r19.9rmv 3373 opabm 4107 eliunxp 4575 relop 4586 dmuni 4646 dmres 4734 dminss 4846 imainss 4847 ssrnres 4873 cnvresima 4920 resco 4935 rnco 4937 coass 4949 xpcom 4977 f11o 5286 fvelrnb 5352 rnoprab 5731 domen 6466 xpassen 6544 genpassl 7081 genpassu 7082 |
Copyright terms: Public domain | W3C validator |