Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 23-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | exlimd.1 | |
|
exlimd.2 | |
||
exlimd.3 | |
||
Assertion | exlimd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimd.1 | |
|
2 | exlimd.2 | |
|
3 | exlimd.3 | |
|
4 | 1 3 | eximd | |
5 | 2 | 19.9 | |
6 | 4 5 | syl6ib | |