# Metamath Proof Explorer

## Theorem 19.41v

Description: Version of 19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

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

### Proof

Step Hyp Ref Expression
1 19.40 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
2 ax5e ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to {\psi }$
3 2 anim2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)$
4 1 3 syl ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)$
5 pm3.21 ${⊢}{\psi }\to \left({\phi }\to \left({\phi }\wedge {\psi }\right)\right)$
6 5 eximdv ${⊢}{\psi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\right)$
7 6 impcom ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
8 4 7 impbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)$