Theorem moani

Description: "At most one" is still true when a conjunct is added, inference form. (Contributed by NM, 9-Mar-1995)

	Ref	Expression
Hypothesis	moani.1	|- E* x ph
Assertion	moani	|- E* x ( ps /\ ph )

Proof

Step	Hyp	Ref	Expression
1		moani.1	|- E* x ph
2		moan	|- ( E* x ph -> E* x ( ps /\ ph ) )
3	1 2	ax-mp	|- E* x ( ps /\ ph )