Theorem rexlimdvaa 2624

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  rexlimddv  2628  nnsucuniel  6581  omp1eomlem  7196  ctmlemr  7210  mulgt0sr  7891  axpre-suploclemres  8014  cnegex  8250  receuap  8742  recapb  8744  rexanuz  11299  climcaucn  11662  fsumiun  11788  dvdsval2  12101  nninfctlemfo  12361  prmind2  12442  pcprmpw2  12656  pockthg  12680  dvdsrvald  13855  dvdsrd  13856  dvdsrex  13860  unitgrp  13878  isnzr2  13946  znunit  14421  tgcl  14536  neiint  14617  restopnb  14653  iscnp4  14690  blssexps  14901  blssex  14902  lgsne0  15515  lgsquadlem1  15554