# Metamath Proof Explorer

## Theorem exdistrv

Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v and 19.42v . For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv . (Contributed by BJ, 30-Sep-2022)

Ref Expression
Assertion exdistrv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 exdistr ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
2 19.41v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 1 2 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$