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  6550  omp1eomlem  7155  ctmlemr  7169  mulgt0sr  7840  axpre-suploclemres  7963  cnegex  8199  receuap  8690  recapb  8692  rexanuz  11135  climcaucn  11497  fsumiun  11623  dvdsval2  11936  nninfctlemfo  12180  prmind2  12261  pcprmpw2  12474  pockthg  12498  dvdsrvald  13592  dvdsrd  13593  dvdsrex  13597  unitgrp  13615  isnzr2  13683  znunit  14158  tgcl  14243  neiint  14324  restopnb  14360  iscnp4  14397  blssexps  14608  blssex  14609  lgsne0  15195  lgsquadlem1  15234