Theorem reximddv

Description: Deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		reximddva.1	|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )
2		reximddva.2	|- ( ph -> E. x e. A ps )
3	1	expr	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
4	3	reximdva	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
5	2 4	mpd	|- ( ph -> E. x e. A ch )