Theorem moimdv

The at-most-one quantifier reverses implication, deduction form. (Contributed by Thierry Arnoux, 25-Feb-2017.)

Hypothesis
moimdv.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \exists^\ast x \, \chi \rightarrow \exists^\ast x \, \psi \)
Proof
moimdv.1
l1
alrimiv _
\( \vdash \varphi \rightarrow \forall x \, (\psi \rightarrow \chi) \)
moim
\( \vdash \forall x \, (\psi \rightarrow \chi) \rightarrow \exists^\ast x \, \chi \rightarrow \exists^\ast x \, \psi \)
syl l1 _