# Metamath Proof Explorer

## Theorem aleximi

Description: A variant of al2imi : instead of applying A. x quantifiers to the final implication, replace them with E. x . A shorter proof is possible using nfa1 , sps and eximd , but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019)

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

### Proof

Step Hyp Ref Expression
1 aleximi.1 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
2 1 con3d ${⊢}{\phi }\to \left(¬{\chi }\to ¬{\psi }\right)$
3 2 al2imi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }\right)$
4 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\chi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }$
5 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }$
6 3 4 5 3imtr3g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(¬\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
7 6 con4d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$