Theorem rexlimdva2 2654

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  ctssdclemn0  7352  ctssdc  7355  suplocexprlemru  7982  suplocexprlemloc  7984  suplocsrlemb  8069  aptap  8872  4sqlemffi  13032  4sqleminfi  13033  4sqexercise2  13035  4sqlemsdc  13036  ennnfonelemhom  13099  gsumfzval  13537  innei  14957  ivthinclemlr  15431  ivthinclemur  15433  limccnpcntop  15469  limccoap  15472  2lgslem1c  15892  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  umgrnloop  16040