Theorem rexlimdvaa 2615

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  rexlimddv  2619  nnsucuniel  6562  omp1eomlem  7169  ctmlemr  7183  mulgt0sr  7864  axpre-suploclemres  7987  cnegex  8223  receuap  8715  recapb  8717  rexanuz  11172  climcaucn  11535  fsumiun  11661  dvdsval2  11974  nninfctlemfo  12234  prmind2  12315  pcprmpw2  12529  pockthg  12553  dvdsrvald  13727  dvdsrd  13728  dvdsrex  13732  unitgrp  13750  isnzr2  13818  znunit  14293  tgcl  14408  neiint  14489  restopnb  14525  iscnp4  14562  blssexps  14773  blssex  14774  lgsne0  15387  lgsquadlem1  15426