# Metamath Proof Explorer

## Theorem exlimddvf

Description: A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019)

Ref Expression
Hypotheses exlimddvf.1 ${⊢}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\theta }$
exlimddvf.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
exlimddvf.3 ${⊢}\left({\theta }\wedge {\psi }\right)\to {\chi }$
exlimddvf.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
Assertion exlimddvf ${⊢}\left({\phi }\wedge {\psi }\right)\to {\chi }$

### Proof

Step Hyp Ref Expression
1 exlimddvf.1 ${⊢}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\theta }$
2 exlimddvf.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 exlimddvf.3 ${⊢}\left({\theta }\wedge {\psi }\right)\to {\chi }$
4 exlimddvf.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
5 3 expcom ${⊢}{\psi }\to \left({\theta }\to {\chi }\right)$
6 2 4 5 exlimd ${⊢}{\psi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\theta }\to {\chi }\right)$
7 1 6 mpan9 ${⊢}\left({\phi }\wedge {\psi }\right)\to {\chi }$