Theorem exlimddvf

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

	Ref	Expression
Hypotheses	exlimddvf.1	$$⊢\phi \to \exists x\theta$$
	exlimddvf.2	$$⊢Ⅎx\psi$$
	exlimddvf.3	$$⊢\left(\theta \wedge \psi \right)\to \chi$$
	exlimddvf.4	$$⊢Ⅎx\chi$$
Assertion	exlimddvf	$$⊢\left(\phi \wedge \psi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		exlimddvf.1	$$⊢\phi \to \exists x\theta$$
2		exlimddvf.2	$$⊢Ⅎx\psi$$
3		exlimddvf.3	$$⊢\left(\theta \wedge \psi \right)\to \chi$$
4		exlimddvf.4	$$⊢Ⅎx\chi$$
5	3	expcom	$$⊢\psi \to \left(\theta \to \chi \right)$$
6	2 4 5	exlimd	$$⊢\psi \to \left(\exists x\theta \to \chi \right)$$
7	1 6	mpan9	$$⊢\left(\phi \wedge \psi \right)\to \chi$$