# Metamath Proof Explorer

## Theorem rexlimdvv

Description: Inference from Theorem 19.23 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004)

Ref Expression
Hypothesis rexlimdvv.1 ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({\psi }\to {\chi }\right)\right)$
Assertion rexlimdvv ${⊢}{\phi }\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\to {\chi }\right)$

### Proof

Step Hyp Ref Expression
1 rexlimdvv.1 ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({\psi }\to {\chi }\right)\right)$
2 1 expdimp ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({y}\in {B}\to \left({\psi }\to {\chi }\right)\right)$
3 2 rexlimdv ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\to {\chi }\right)$
4 3 rexlimdva ${⊢}{\phi }\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\to {\chi }\right)$