Theorem
moan
"At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
Conclusion
\( \vdash \exists^\ast x \, \varphi \rightarrow \exists^\ast x \, (\psi \wedge \varphi) \)
Proof
simpr
moimi
_
This is the content in the right pane.