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	⊢ ( 𝜑 → 𝜓 )
	spesbcdi.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜒 ↔ 𝜓 )
Assertion	spesbcdi	⊢ ( 𝜑 → ∃ 𝑥 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		spesbcdi.1	⊢ ( 𝜑 → 𝜓 )
2		spesbcdi.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜒 ↔ 𝜓 )
3	1 2	sylibr	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 )
4	3	spesbcd	⊢ ( 𝜑 → ∃ 𝑥 𝜒 )