# Metamath Proof Explorer

## Theorem 4exdistrv

Description: Distribute two pairs of existential quantifiers (over disjoint variables) over a conjunction. For a version with fewer disjoint variable conditions but requiring more axioms, see ee4anv . (Contributed by BJ, 5-Jan-2023)

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

### Proof

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