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	$$⊢\phi \to \exists x\theta$$
	exlimddvfi.2	$$⊢Ⅎy\theta$$
	exlimddvfi.3	$$⊢Ⅎy\psi$$
	exlimddvfi.4	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\theta \leftrightarrow \eta$$
	exlimddvfi.5	$$⊢\left(\eta \wedge \psi \right)\to \chi$$
	exlimddvfi.6	$$⊢Ⅎy\chi$$
Assertion	exlimddvfi	$$⊢\left(\phi \wedge \psi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		exlimddvfi.1	$$⊢\phi \to \exists x\theta$$
2		exlimddvfi.2	$$⊢Ⅎy\theta$$
3		exlimddvfi.3	$$⊢Ⅎy\psi$$
4		exlimddvfi.4	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\theta \leftrightarrow \eta$$
5		exlimddvfi.5	$$⊢\left(\eta \wedge \psi \right)\to \chi$$
6		exlimddvfi.6	$$⊢Ⅎy\chi$$
7	2	sb8e	$$⊢\exists x\theta \leftrightarrow \exists y\left[y/x\right]\theta$$
8	1 7	sylib	$$⊢\phi \to \exists y\left[y/x\right]\theta$$
9		sbsbc	$$⊢\left[y/x\right]\theta \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\theta$$
10	9 4	bitri	$$⊢\left[y/x\right]\theta \leftrightarrow \eta$$
11	10 5	sylanb	$$⊢\left(\left[y/x\right]\theta \wedge \psi \right)\to \chi$$
12	8 3 11 6	exlimddvf	$$⊢\left(\phi \wedge \psi \right)\to \chi$$