Theorem moanimv

Introduction of a conjunct into an at-most-one quantifier. Version of moanim requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995.) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023.)

Conclusion
\( \vdash \exists^\ast x \, (\varphi \wedge \psi) \leftrightarrow \varphi \rightarrow \exists^\ast x \, \psi \)
Proof
ibar
l1
mobidv _
simpl
exlimiv _
moanimlem l1 _