Theorem rexlimdva2 2625

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Hypothesis

Ref	Expression
rexlimdva2.1	|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )

Assertion

Ref	Expression
rexlimdva2	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ch, x   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdva2

Step	Hyp	Ref	Expression
1		rexlimdva2.1	. . 3 |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
2	1	exp31 364	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2621	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2175   E.wrex 2484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488  df-rex 2489

This theorem is referenced by:  ctssdclemn0  7211  ctssdc  7214  suplocexprlemru  7831  suplocexprlemloc  7833  suplocsrlemb  7918  aptap  8722  4sqlemffi  12690  4sqleminfi  12691  4sqexercise2  12693  4sqlemsdc  12694  ennnfonelemhom  12757  gsumfzval  13194  reldvdsrsrg  13825  innei  14606  ivthinclemlr  15080  ivthinclemur  15082  limccnpcntop  15118  limccoap  15121  2lgslem1c  15538  2lgslem3a1  15545  2lgslem3b1  15546  2lgslem3c1  15547  2lgslem3d1  15548