![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > reximdv | Unicode version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.) |
Ref | Expression |
---|---|
reximdv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
reximdv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1d 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | reximdvai 2587 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-4 1520 ax-17 1536 ax-ial 1544 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-ral 2470 df-rex 2471 |
This theorem is referenced by: r19.12 2593 reusv3 4472 rexxfrd 4475 iunpw 4492 fvelima 5580 carden2bex 7202 prnmaddl 7503 prarloclem5 7513 prarloc2 7517 genprndl 7534 genprndu 7535 ltpopr 7608 recexprlemm 7637 recexprlemopl 7638 recexprlemopu 7640 recexprlem1ssl 7646 recexprlem1ssu 7647 cauappcvgprlemupu 7662 caucvgprlemupu 7685 caucvgprprlemupu 7713 caucvgsrlemoffres 7813 map2psrprg 7818 resqrexlemgt0 11043 subcn2 11333 bezoutlembz 12019 pythagtriplem19 12296 tgcl 13917 neiss 14003 ssnei2 14010 tgcnp 14062 cnptopco 14075 cnptopresti 14091 lmtopcnp 14103 blssexps 14282 blssex 14283 mopni3 14337 neibl 14344 metss 14347 metcnp3 14364 rescncf 14421 limcresi 14488 |
Copyright terms: Public domain | W3C validator |