Theorem moanim

Introduction of a conjunct into "at most one" quantifier. For a version requiring disjoint variables, but fewer axioms, see moanimv. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 24-Dec-2018.)

Hypothesis
moanim.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \exists^\ast x \, (\varphi \wedge \psi) \leftrightarrow \varphi \rightarrow \exists^\ast x \, \psi \)
Proof
l0
moanim.1
ibar
l2
mobid l0 _
l3
moanim.1
simpl
exlimi l3 _
moanimlem l2 _