Theorem moanimlem

Description: 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)

	Ref	Expression
Hypotheses	moanimlem.1	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow {\exists }^{*}x\left(\phi \wedge \psi \right)\right)$$
	moanimlem.2	$$⊢\exists x\left(\phi \wedge \psi \right)\to \phi$$
Assertion	moanimlem	$$⊢{\exists }^{*}x\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \to {\exists }^{*}x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		moanimlem.1	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow {\exists }^{*}x\left(\phi \wedge \psi \right)\right)$$
2		moanimlem.2	$$⊢\exists x\left(\phi \wedge \psi \right)\to \phi$$
3	1	biimprcd	$$⊢{\exists }^{*}x\left(\phi \wedge \psi \right)\to \left(\phi \to {\exists }^{*}x\psi \right)$$
4		nexmo	$$⊢\neg \exists x\left(\phi \wedge \psi \right)\to {\exists }^{*}x\left(\phi \wedge \psi \right)$$
5	2 4	nsyl5	$$⊢\neg \phi \to {\exists }^{*}x\left(\phi \wedge \psi \right)$$
6		moan	$$⊢{\exists }^{*}x\psi \to {\exists }^{*}x\left(\phi \wedge \psi \right)$$
7	5 6	ja	$$⊢\left(\phi \to {\exists }^{*}x\psi \right)\to {\exists }^{*}x\left(\phi \wedge \psi \right)$$
8	3 7	impbii	$$⊢{\exists }^{*}x\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \to {\exists }^{*}x\psi \right)$$