Theorem moanmo

Description: Nested at-most-one quantifiers. (Contributed by NM, 25-Jan-2006)

	Ref	Expression
Assertion	moanmo	|- E* x ( ph /\ E* x ph )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( E* x ph -> E* x ph )
2		nfmo1	|- F/ x E* x ph
3	2	moanim	|- ( E* x ( E* x ph /\ ph ) <-> ( E* x ph -> E* x ph ) )
4	1 3	mpbir	|- E* x ( E* x ph /\ ph )
5		ancom	|- ( ( ph /\ E* x ph ) <-> ( E* x ph /\ ph ) )
6	5	mobii	|- ( E* x ( ph /\ E* x ph ) <-> E* x ( E* x ph /\ ph ) )
7	4 6	mpbir	|- E* x ( ph /\ E* x ph )