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	|- ( ph -> ( E* x ps <-> E* x ( ph /\ ps ) ) )
	moanimlem.2	|- ( E. x ( ph /\ ps ) -> ph )
Assertion	moanimlem	|- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )

Proof

Step	Hyp	Ref	Expression
1		moanimlem.1	|- ( ph -> ( E* x ps <-> E* x ( ph /\ ps ) ) )
2		moanimlem.2	|- ( E. x ( ph /\ ps ) -> ph )
3	1	biimprcd	|- ( E* x ( ph /\ ps ) -> ( ph -> E* x ps ) )
4		nexmo	|- ( -. E. x ( ph /\ ps ) -> E* x ( ph /\ ps ) )
5	2 4	nsyl5	|- ( -. ph -> E* x ( ph /\ ps ) )
6		moan	|- ( E* x ps -> E* x ( ph /\ ps ) )
7	5 6	ja	|- ( ( ph -> E* x ps ) -> E* x ( ph /\ ps ) )
8	3 7	impbii	|- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )