# Metamath Proof Explorer

## Theorem 19.37

Description: Theorem 19.37 of Margaris p. 90. See 19.37v for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis 19.37.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion 19.37 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 19.37.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 19.35 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 1 19.3 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔{\phi }$
4 3 imbi1i ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left({\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 2 4 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$