Theorem reximdd

Description: Deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		reximdd.1	$$⊢Ⅎx\phi$$
2		reximdd.2	$$⊢\left(\phi \wedge x\in A\wedge \psi \right)\to \chi$$
3		reximdd.3	$$⊢\phi \to \exists x\in A\psi$$
4	2	3exp	$$⊢\phi \to \left(x\in A\to \left(\psi \to \chi \right)\right)$$
5	1 4	reximdai	$$⊢\phi \to \left(\exists x\in A\psi \to \exists x\in A\chi \right)$$
6	3 5	mpd	$$⊢\phi \to \exists x\in A\chi$$