Theorem exlimddvf

Description: A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019)

	Ref	Expression
Hypotheses	exlimddvf.1	|- ( ph -> E. x th )
	exlimddvf.2	|- F/ x ps
	exlimddvf.3	|- ( ( th /\ ps ) -> ch )
	exlimddvf.4	|- F/ x ch
Assertion	exlimddvf	|- ( ( ph /\ ps ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		exlimddvf.1	|- ( ph -> E. x th )
2		exlimddvf.2	|- F/ x ps
3		exlimddvf.3	|- ( ( th /\ ps ) -> ch )
4		exlimddvf.4	|- F/ x ch
5	3	expcom	|- ( ps -> ( th -> ch ) )
6	2 4 5	exlimd	|- ( ps -> ( E. x th -> ch ) )
7	1 6	mpan9	|- ( ( ph /\ ps ) -> ch )