Theorem reximdvai 2897

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 2837	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
3		rexim 2890	. 2 |- ( A. x e. A ( ps -> ch ) -> ( E. x e. A ps -> E. x e. A ch ) )
4	2, 3	syl 17	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1868   A.wral 2775   E.wrex 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781

This theorem is referenced by:  reximdv  2899  reximdva  2900  reuind  3275  wefrc  4843  isomin  6239  isofrlem  6242  onfununi  7064  oaordex  7263  odi  7284  omass  7285  omeulem1  7287  noinfep  8166  rankwflemb  8265  infxpenlem  8445  coflim  8691  coftr  8703  zorn2lem7  8932  suplem1pr  9477  axpre-sup  9593  climbdd  13720  filufint  20919  cvati  28002  atcvat4i  28033  mdsymlem2  28040  mdsymlem3  28041  sumdmdii  28051  iccllyscon  29966  dftrpred3g  30466  incsequz2  31989  lcvat  32512  hlrelat3  32893  cvrval3  32894  cvrval4N  32895  2atlt  32920  cvrat4  32924  atbtwnexOLDN  32928  atbtwnex  32929  athgt  32937  2llnmat  33005  lnjatN  33261  2lnat  33265  cdlemb  33275  lhpexle3lem  33492  cdlemf1  34044  cdlemf2  34045  cdlemf  34046  cdlemk26b-3  34388  dvh4dimlem  34927  upbdrech  37362  limcperiod  37525  cncfshift  37568  cncfperiod  37573