![]() |
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 2473 |
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 df-nf 1395 df-ral 2364 df-rex 2365 |
This theorem is referenced by: r19.12 2478 reusv3 4282 rexxfrd 4285 iunpw 4302 fvelima 5356 carden2bex 6817 prnmaddl 7049 prarloclem5 7059 prarloc2 7063 genprndl 7080 genprndu 7081 ltpopr 7154 recexprlemm 7183 recexprlemopl 7184 recexprlemopu 7186 recexprlem1ssl 7192 recexprlem1ssu 7193 cauappcvgprlemupu 7208 caucvgprlemupu 7231 caucvgprprlemupu 7259 caucvgsrlemoffres 7345 resqrexlemgt0 10453 subcn2 10700 bezoutlembz 11271 rescncf 11637 |
Copyright terms: Public domain | W3C validator |