# Metamath Proof Explorer

## Theorem 19.25

Description: Theorem 19.25 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)

Ref Expression
Assertion 19.25 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 biimpi ${⊢}\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)$
3 2 aleximi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$