Theorem moimi

The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.)

Hypothesis
moimi.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \exists^\ast x \, \psi \rightarrow \exists^\ast x \, \varphi \)
Proof
l0
moim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists^\ast x \, \psi \rightarrow \exists^\ast x \, \varphi \)
moimi.1
\( \vdash \varphi \rightarrow \psi \)
mpg l0 _