Theorem rexlimdvaa 2623

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

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

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488  df-rex 2489

This theorem is referenced by:  rexlimddv  2627  nnsucuniel  6580  omp1eomlem  7195  ctmlemr  7209  mulgt0sr  7890  axpre-suploclemres  8013  cnegex  8249  receuap  8741  recapb  8743  rexanuz  11270  climcaucn  11633  fsumiun  11759  dvdsval2  12072  nninfctlemfo  12332  prmind2  12413  pcprmpw2  12627  pockthg  12651  dvdsrvald  13826  dvdsrd  13827  dvdsrex  13831  unitgrp  13849  isnzr2  13917  znunit  14392  tgcl  14507  neiint  14588  restopnb  14624  iscnp4  14661  blssexps  14872  blssex  14873  lgsne0  15486  lgsquadlem1  15525