Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimi | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) |
Ref | Expression |
---|---|
ralrimi.1 | |
ralrimi.2 |
Ref | Expression |
---|---|
ralrimi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimi.1 | . . 3 | |
2 | ralrimi.2 | . . 3 | |
3 | 1, 2 | alrimi 1502 | . 2 |
4 | df-ral 2440 | . 2 | |
5 | 3, 4 | sylibr 133 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1333 wnf 1440 wcel 2128 wral 2435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 ax-4 1490 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-ral 2440 |
This theorem is referenced by: ralrimiv 2529 reximdai 2555 r19.12 2563 rexlimd 2571 rexlimd2 2572 r19.29af2 2597 r19.37 2609 ralidm 3495 iineq2d 3871 mpteq2da 4055 onintonm 4478 mpteqb 5560 fmptdf 5626 eusvobj2 5812 tfri3 6316 mapxpen 6795 fodjuomnilemdc 7089 cc3 7190 fimaxre2 11137 fprodcllemf 11521 fprodap0f 11544 fprodle 11548 zsupcllemstep 11844 bezoutlemmain 11897 bezoutlemzz 11901 exmidunben 12225 mulcncf 13061 limccnp2lem 13115 |
Copyright terms: Public domain | W3C validator |