Theorem reximd2a

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020)

	Ref	Expression
Hypotheses	reximd2a.1	|- F/ x ph
	reximd2a.2	|- ( ( ( ph /\ x e. A ) /\ ps ) -> x e. B )
	reximd2a.3	|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
	reximd2a.4	|- ( ph -> E. x e. A ps )
Assertion	reximd2a	|- ( ph -> E. x e. B ch )

Proof

Step	Hyp	Ref	Expression
1		reximd2a.1	|- F/ x ph
2		reximd2a.2	|- ( ( ( ph /\ x e. A ) /\ ps ) -> x e. B )
3		reximd2a.3	|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
4		reximd2a.4	|- ( ph -> E. x e. A ps )
5	2 3	jca	|- ( ( ( ph /\ x e. A ) /\ ps ) -> ( x e. B /\ ch ) )
6	5	expl	|- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )
7	1 6	eximd	|- ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
8		df-rex	|- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
9		df-rex	|- ( E. x e. B ch <-> E. x ( x e. B /\ ch ) )
10	7 8 9	3imtr4g	|- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )
11	4 10	mpd	|- ( ph -> E. x e. B ch )