# Metamath Proof Explorer

## Theorem reximdvva

Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by AV, 5-Jan-2022)

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

### Proof

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