Theorem reximddv2

Description: Double deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	reximddv2.1	|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ ps ) -> ch )
	reximddv2.2	|- ( ph -> E. x e. A E. y e. B ps )
Assertion	reximddv2	|- ( ph -> E. x e. A E. y e. B ch )

Proof

Step	Hyp	Ref	Expression
1		reximddv2.1	|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ ps ) -> ch )
2		reximddv2.2	|- ( ph -> E. x e. A E. y e. B ps )
3	1	ex	|- ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ps -> ch ) )
4	3	reximdva	|- ( ( ph /\ x e. A ) -> ( E. y e. B ps -> E. y e. B ch ) )
5	4	impr	|- ( ( ph /\ ( x e. A /\ E. y e. B ps ) ) -> E. y e. B ch )
6	5 2	reximddv	|- ( ph -> E. x e. A E. y e. B ch )