Description: Double deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | reximddv2.1 | ||
reximddv2.2 | |||
Assertion | reximddv2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximddv2.1 | ||
2 | reximddv2.2 | ||
3 | 1 | ex | |
4 | 3 | reximdva | |
5 | 4 | impr | |
6 | 5 2 | reximddv |