Theorem rexlimdvaa 2612

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  rexlimddv  2616  nnsucuniel  6548  omp1eomlem  7153  ctmlemr  7167  mulgt0sr  7838  axpre-suploclemres  7961  cnegex  8197  receuap  8688  recapb  8690  rexanuz  11132  climcaucn  11494  fsumiun  11620  dvdsval2  11933  nninfctlemfo  12177  prmind2  12258  pcprmpw2  12471  pockthg  12495  dvdsrvald  13589  dvdsrd  13590  dvdsrex  13594  unitgrp  13612  isnzr2  13680  znunit  14147  tgcl  14232  neiint  14313  restopnb  14349  iscnp4  14386  blssexps  14597  blssex  14598  lgsne0  15154  lgsquadlem1  15191