# Metamath Proof Explorer

## Theorem 19.35

Description: Theorem 19.35 of Margaris p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 27-Jun-2014)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 pm2.27 ${⊢}{\phi }\to \left(\left({\phi }\to {\psi }\right)\to {\psi }\right)$
2 1 aleximi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 2 com12 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
4 exnal ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 pm2.21 ${⊢}¬{\phi }\to \left({\phi }\to {\psi }\right)$
6 5 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
7 4 6 sylbir ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
8 exa1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
9 7 8 ja ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
10 3 9 impbii ${⊢}\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)$