# Metamath Proof Explorer

## Theorem r19.29d2r

Description: Theorem 19.29 of Margaris p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017)

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

### Proof

Step Hyp Ref Expression
1 r19.29d2r.1 ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
2 r19.29d2r.2 ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }$
3 r19.29 ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 1 2 3 syl2anc ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 r19.29 ${⊢}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)$
6 5 reximi ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)$
7 4 6 syl ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)$