# Metamath Proof Explorer

## Theorem exlimd

Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 23-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jan-2018)

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

### Proof

Step Hyp Ref Expression
1 exlimd.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 exlimd.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
3 exlimd.3 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
4 1 3 eximd ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 2 19.9 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }↔{\chi }$
6 4 5 syl6ib ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to {\chi }\right)$