Theorem rexlimdva2 2665

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

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

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 2527  df-rex 2528

This theorem is referenced by:  ctssdclemn0  7414  ctssdc  7417  suplocexprlemru  8050  suplocexprlemloc  8052  suplocsrlemb  8137  aptap  8941  4sqlemffi  13119  4sqleminfi  13120  4sqexercise2  13122  4sqlemsdc  13123  ennnfonelemhom  13250  gsumfzval  13654  innei  15154  ivthinclemlr  15628  ivthinclemur  15630  limccnpcntop  15666  limccoap  15669  2lgslem1c  16089  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  umgrnloop  16237