# Metamath Proof Explorer

## Theorem 19.42v

Description: Version of 19.42 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993)

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

### Proof

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