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 2461 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1433 wrex 2349 |
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 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-ral 2353 df-rex 2354 |
This theorem is referenced by: r19.12 2466 reusv3 4210 rexxfrd 4213 iunpw 4229 fvelima 5246 carden2bex 6458 prnmaddl 6680 prarloclem5 6690 prarloc2 6694 genprndl 6711 genprndu 6712 ltpopr 6785 recexprlemm 6814 recexprlemopl 6815 recexprlemopu 6817 recexprlem1ssl 6823 recexprlem1ssu 6824 cauappcvgprlemupu 6839 caucvgprlemupu 6862 caucvgprprlemupu 6890 caucvgsrlemoffres 6976 resqrexlemgt0 9906 subcn2 10150 bezoutlembz 10393 |
Copyright terms: Public domain | W3C validator |