Description: Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997) (Proof shortened by Wolf Lammen, 1-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | ralim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |
|
2 | 1 | ral2imi | |