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 1487 | . 2 |
4 | df-ral 2398 | . 2 | |
5 | 3, 4 | sylibr 133 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1314 wnf 1421 wcel 1465 wral 2393 |
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 1408 ax-gen 1410 ax-4 1472 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 |
This theorem is referenced by: ralrimiv 2481 reximdai 2507 r19.12 2515 rexlimd 2523 rexlimd2 2524 r19.29af2 2549 r19.37 2560 ralidm 3433 iineq2d 3803 mpteq2da 3987 onintonm 4403 mpteqb 5479 fmptdf 5545 eusvobj2 5728 tfri3 6232 mapxpen 6710 fodjuomnilemdc 6984 fimaxre2 10966 zsupcllemstep 11565 bezoutlemmain 11613 bezoutlemzz 11617 exmidunben 11866 mulcncf 12687 limccnp2lem 12741 |
Copyright terms: Public domain | W3C validator |