Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of Margaris p. 90. (Contributed by NM, 22-Sep-2003) (Proof shortened by Wolf Lammen, 29-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ralimdaa.1 | |
|
ralimdaa.2 | |
||
Assertion | ralimdaa | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdaa.1 | |
|
2 | ralimdaa.2 | |
|
3 | 2 | ex | |
4 | 1 3 | ralrimi | |
5 | ralim | |
|
6 | 4 5 | syl | |