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 | |