Theorem exellimddv

Description: Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020)

	Ref	Expression
Hypotheses	exellimddv.1	|- ( ph -> E. x x e. A )
	exellimddv.2	|- ( ph -> ( x e. A -> ps ) )
Assertion	exellimddv	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		exellimddv.1	|- ( ph -> E. x x e. A )
2		exellimddv.2	|- ( ph -> ( x e. A -> ps ) )
3	2	alrimiv	|- ( ph -> A. x ( x e. A -> ps ) )
4		exellim	|- ( ( E. x x e. A /\ A. x ( x e. A -> ps ) ) -> ps )
5	1 3 4	syl2anc	|- ( ph -> ps )