Theorem reximdvai 2913

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 2853	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
3		rexim 2906	. 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 1802   A.wral 2791   E.wrex 2792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-ral 2796  df-rex 2797

This theorem is referenced by:  reximdv  2915  reximdva  2916  reuind  3287  wefrc  4860  isomin  6215  isofrlem  6218  onfununi  7011  oaordex  7206  odi  7227  omass  7228  omeulem1  7230  noinfep  8076  rankwflemb  8211  infxpenlem  8391  coflim  8641  coftr  8653  zorn2lem7  8882  suplem1pr  9430  axpre-sup  9546  climbdd  13470  filufint  20291  cvati  27154  atcvat4i  27185  mdsymlem2  27192  mdsymlem3  27193  sumdmdii  27203  iccllyscon  28565  dftrpred3g  29288  incsequz2  30214  upbdrech  31454  limcperiod  31542  cncfshift  31583  cncfperiod  31588  lcvat  34478  hlrelat3  34859  cvrval3  34860  cvrval4N  34861  2atlt  34886  cvrat4  34890  atbtwnexOLDN  34894  atbtwnex  34895  athgt  34903  2llnmat  34971  lnjatN  35227  2lnat  35231  cdlemb  35241  lhpexle3lem  35458  cdlemf1  36010  cdlemf2  36011  cdlemf  36012  cdlemk26b-3  36354  dvh4dimlem  36893