Theorem moani

"At most one" is still true when a conjunct is added, inference form. (Contributed by NM, 9-Mar-1995.)

Hypothesis
moani.1
\( \vdash \exists^\ast x \, \varphi \)
Conclusion
\( \vdash \exists^\ast x \, (\psi \wedge \varphi) \)
Proof
l0
moani.1
\( \vdash \exists^\ast x \, \varphi \)
moan
\( \vdash \exists^\ast x \, \varphi \rightarrow \exists^\ast x \, (\psi \wedge \varphi) \)
ax-mp l0 _