Theorem moa1

If an implication holds for at most one value, then its consequent holds for at most one value. See also ala1 and exa1. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Wolf Lammen, 22-Dec-2018.)

Conclusion
\( \vdash \exists^\ast x \, (\varphi \rightarrow \psi) \rightarrow \exists^\ast x \, \psi \)
Proof
ax-1
moimi _