# Metamath Proof Explorer

## Theorem bj-exalimi

Description: An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim (using mpg ) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw proves. (Contributed by BJ, 29-Sep-2019)

Ref Expression
Hypothesis bj-exalimi.1 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
Assertion bj-exalimi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 bj-exalimi.1 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
2 1 com12 ${⊢}{\psi }\to \left({\phi }\to {\chi }\right)$
3 2 aleximi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 3 com12 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$