Theorem moanimlem

Factor out the common proof skeleton of moanimv and moanim. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 24-Dec-2018.) Factor out common proof lines. (Revised by Wolf Lammen, 8-Feb-2023.)

Hypotheses
moanimlem.1
\( \vdash \varphi \rightarrow (\exists^\ast x \, \psi \leftrightarrow \exists^\ast x \, (\varphi \wedge \psi)) \)
moanimlem.2
\( \vdash \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \)
Conclusion
\( \vdash \exists^\ast x \, (\varphi \wedge \psi) \leftrightarrow \varphi \rightarrow \exists^\ast x \, \psi \)
Proof
moanimlem.1
l1
biimprcd _
l2
moanimlem.2
\( \vdash \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \)
nexmo
\( \vdash \neg \exists x \, (\varphi \wedge \psi) \rightarrow \exists^\ast x \, (\varphi \wedge \psi) \)
l4
nsyl5 l2 _
moan
ja l4 _
impbii l1 _