![]() |
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 1533 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-ral 2473 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | sylibr 134 |
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 1458 ax-gen 1460 ax-4 1521 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 |
This theorem is referenced by: ralrimiv 2562 reximdai 2588 r19.12 2596 rexlimd 2604 rexlimd2 2605 r19.29af2 2630 r19.37 2642 ralidm 3538 iineq2d 3921 mpteq2da 4107 onintonm 4534 mpteqb 5626 fmptdf 5693 eusvobj2 5881 tfri3 6391 mapxpen 6875 fodjuomnilemdc 7171 cc3 7296 fimaxre2 11266 fprodcllemf 11652 fprodap0f 11675 fprodle 11679 zsupcllemstep 11977 bezoutlemmain 12030 bezoutlemzz 12034 exmidunben 12476 mulcncf 14543 limccnp2lem 14597 |
Copyright terms: Public domain | W3C validator |