Theorem rexlimdvaa 2595

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypothesis

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

Assertion

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

Distinct variable groups:   ph, x   ch, x

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

Proof of Theorem rexlimdvaa

Step	Hyp	Ref	Expression
1		rexlimdvaa.1	. . 3 |- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )
2	1	expr 375	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	rexlimdva 2594	1 |- ( ph -> ( E. x e. A ps -> ch ) )

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  rexlimddv  2599  nnsucuniel  6498  omp1eomlem  7095  ctmlemr  7109  mulgt0sr  7779  axpre-suploclemres  7902  cnegex  8137  receuap  8628  recapb  8630  rexanuz  10999  climcaucn  11361  fsumiun  11487  dvdsval2  11799  prmind2  12122  pcprmpw2  12334  pockthg  12357  dvdsrvald  13267  dvdsrd  13268  dvdsrex  13272  unitgrp  13290  tgcl  13603  neiint  13684  restopnb  13720  iscnp4  13757  blssexps  13968  blssex  13969  lgsne0  14478