Theorem rexlimdvaa 2669

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  rexlimddv  2673  nnsucuniel  6758  omp1eomlem  7424  ctmlemr  7438  mulgt0sr  8135  axpre-suploclemres  8258  cnegex  8494  receuap  8989  recapb  8991  rexanuz  11732  climcaucn  12095  fsumiun  12222  dvdsval2  12535  nninfctlemfo  12795  prmind2  12876  pcprmpw2  13090  pockthg  13114  dvdsrvald  14373  dvdsrd  14374  dvdsrex  14378  unitgrp  14396  isnzr2  14464  znunit  14966  tgcl  15088  neiint  15169  restopnb  15205  iscnp4  15242  blssexps  15453  blssex  15454  lgsne0  16071  lgsquadlem1  16110