Theorem exlimddvfi

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

	Ref	Expression
Hypotheses	exlimddvfi.1	|- ( ph -> E. x th )
	exlimddvfi.2	|- F/ y th
	exlimddvfi.3	|- F/ y ps
	exlimddvfi.4	|- ( [. y / x ]. th <-> et )
	exlimddvfi.5	|- ( ( et /\ ps ) -> ch )
	exlimddvfi.6	|- F/ y ch
Assertion	exlimddvfi	|- ( ( ph /\ ps ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		exlimddvfi.1	|- ( ph -> E. x th )
2		exlimddvfi.2	|- F/ y th
3		exlimddvfi.3	|- F/ y ps
4		exlimddvfi.4	|- ( [. y / x ]. th <-> et )
5		exlimddvfi.5	|- ( ( et /\ ps ) -> ch )
6		exlimddvfi.6	|- F/ y ch
7	2	sb8e	|- ( E. x th <-> E. y [ y / x ] th )
8	1 7	sylib	|- ( ph -> E. y [ y / x ] th )
9		sbsbc	|- ( [ y / x ] th <-> [. y / x ]. th )
10	9 4	bitri	|- ( [ y / x ] th <-> et )
11	10 5	sylanb	|- ( ( [ y / x ] th /\ ps ) -> ch )
12	8 3 11 6	exlimddvf	|- ( ( ph /\ ps ) -> ch )