Theorem reximdvai 2838

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.)

Hypothesis

Ref	Expression
reximdvai.1	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )

Assertion

Ref	Expression
reximdvai	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reximdvai

Step	Hyp	Ref	Expression
1		nfv 1673	. 2 |- F/ x ph
2		reximdvai.1	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	1, 2	reximdai 2836	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1756   E.wrex 2728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2732  df-rex 2733

This theorem is referenced by:  reximdv  2839  reximdva  2840  reuind  3174  wefrc  4726  isomin  6040  isofrlem  6043  onfununi  6814  oaordex  7009  odi  7030  omass  7031  omeulem1  7033  noinfep  7877  rankwflemb  8012  infxpenlem  8192  coflim  8442  coftr  8454  zorn2lem7  8683  suplem1pr  9233  axpre-sup  9348  climbdd  13161  filufint  19505  grpoidinv  23707  cvati  25782  atcvat4i  25813  mdsymlem2  25820  mdsymlem3  25821  sumdmdii  25831  iccllyscon  27151  dftrpred3g  27709  incsequz2  28657  lcvat  32687  hlrelat3  33068  cvrval3  33069  cvrval4N  33070  2atlt  33095  cvrat4  33099  atbtwnexOLDN  33103  atbtwnex  33104  athgt  33112  2llnmat  33180  lnjatN  33436  2lnat  33440  cdlemb  33450  lhpexle3lem  33667  lhpex2leN  33669  cdlemf1  34217  cdlemf2  34218  cdlemf  34219  cdlemg1cex  34244  cdlemk26b-3  34561  dvh4dimlem  35100