Theorem spesbcdi

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

	Ref	Expression
Hypotheses	spesbcdi.1	|- ( ph -> ps )
	spesbcdi.2	|- ( [. A / x ]. ch <-> ps )
Assertion	spesbcdi	|- ( ph -> E. x ch )

Proof

Step	Hyp	Ref	Expression
1		spesbcdi.1	|- ( ph -> ps )
2		spesbcdi.2	|- ( [. A / x ]. ch <-> ps )
3	1 2	sylibr	|- ( ph -> [. A / x ]. ch )
4	3	spesbcd	|- ( ph -> E. x ch )