Theorem exlimd

Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 23-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		exlimd.1	$$⊢Ⅎx\phi$$
2		exlimd.2	$$⊢Ⅎx\chi$$
3		exlimd.3	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	1 3	eximd	$$⊢\phi \to \left(\exists x\psi \to \exists x\chi \right)$$
5	2	19.9	$$⊢\exists x\chi \leftrightarrow \chi$$
6	4 5	imbitrdi	$$⊢\phi \to \left(\exists x\psi \to \chi \right)$$