Theorem exlimdh

Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 28-Jan-1997)

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

Proof

Step	Hyp	Ref	Expression
1		exlimdh.1	$$⊢\phi \to \forall x\phi$$
2		exlimdh.2	$$⊢\chi \to \forall x\chi$$
3		exlimdh.3	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	1	nf5i	$$⊢Ⅎx\phi$$
5	2	nf5i	$$⊢Ⅎx\chi$$
6	4 5 3	exlimd	$$⊢\phi \to \left(\exists x\psi \to \chi \right)$$