Theorem rexlimdva2 2626

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 2622	1 |- ( ph -> ( E. x e. A ps -> ch ) )

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  ctssdclemn0  7212  ctssdc  7215  suplocexprlemru  7832  suplocexprlemloc  7834  suplocsrlemb  7919  aptap  8723  4sqlemffi  12719  4sqleminfi  12720  4sqexercise2  12722  4sqlemsdc  12723  ennnfonelemhom  12786  gsumfzval  13223  reldvdsrsrg  13854  innei  14635  ivthinclemlr  15109  ivthinclemur  15111  limccnpcntop  15147  limccoap  15150  2lgslem1c  15567  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577