Theorem reximdvai 2935

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.)

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		reximdvai.1	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
2	1	ralrimiv 2876	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
3		rexim 2929	. 2 |- ( A. x e. A ( ps -> ch ) -> ( E. x e. A ps -> E. x e. A ch ) )
4	2, 3	syl 16	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1767   A.wral 2814   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820

This theorem is referenced by:  reximdv  2937  reximdva  2938  reuind  3307  wefrc  4873  isomin  6221  isofrlem  6224  onfununi  7012  oaordex  7207  odi  7228  omass  7229  omeulem1  7231  noinfep  8076  rankwflemb  8211  infxpenlem  8391  coflim  8641  coftr  8653  zorn2lem7  8882  suplem1pr  9430  axpre-sup  9546  climbdd  13457  filufint  20184  grpoidinv  24914  cvati  26989  atcvat4i  27020  mdsymlem2  27027  mdsymlem3  27028  sumdmdii  27038  iccllyscon  28363  dftrpred3g  28921  incsequz2  29873  lcvat  33845  hlrelat3  34226  cvrval3  34227  cvrval4N  34228  2atlt  34253  cvrat4  34257  atbtwnexOLDN  34261  atbtwnex  34262  athgt  34270  2llnmat  34338  lnjatN  34594  2lnat  34598  cdlemb  34608  lhpexle3lem  34825  lhpex2leN  34827  cdlemf1  35375  cdlemf2  35376  cdlemf  35377  cdlemg1cex  35402  cdlemk26b-3  35719  dvh4dimlem  36258