# Metamath Proof Explorer

## Theorem reximdd

Description: Deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

### Proof

Step Hyp Ref Expression
1 reximdd.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 reximdd.2 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {\psi }\right)\to {\chi }$
3 reximdd.3 ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$
4 2 3exp ${⊢}{\phi }\to \left({x}\in {A}\to \left({\psi }\to {\chi }\right)\right)$
5 1 4 reximdai ${⊢}{\phi }\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
6 3 5 mpd ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }$