# Metamath Proof Explorer

## Theorem reximddv2

Description: Double deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019)

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

### Proof

Step Hyp Ref Expression
1 reximddv2.1 ${⊢}\left(\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {y}\in {B}\right)\wedge {\psi }\right)\to {\chi }$
2 reximddv2.2 ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
3 1 ex ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {y}\in {B}\right)\to \left({\psi }\to {\chi }\right)$
4 3 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)$
5 4 impr ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }$
6 5 2 reximddv ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }$