Theorem euimOLD

Description: Obsolete version of euim as of 1-Oct-2023. (Contributed by NM, 19-Oct-2005) (Proof shortened by Andrew Salmon, 14-Jun-2011) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	euimOLD	|- ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ( E! x ps -> E! x ph ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1	|- ( E. x ph -> ( E! x ps -> E. x ph ) )
2		euimmo	|- ( A. x ( ph -> ps ) -> ( E! x ps -> E* x ph ) )
3	1 2	anim12ii	|- ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ( E! x ps -> ( E. x ph /\ E* x ph ) ) )
4		df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
5	3 4	syl6ibr	|- ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ( E! x ps -> E! x ph ) )