Theorem reximdvai 2871

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 2812	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
3		rexim 2864	. 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 1898   A.wral 2749   E.wrex 2750

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

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755

This theorem is referenced by:  reximdv  2873  reximdva  2874  reuind  3255  wefrc  4850  isomin  6258  isofrlem  6261  onfununi  7091  oaordex  7290  odi  7311  omass  7312  omeulem1  7314  noinfep  8196  rankwflemb  8295  infxpenlem  8475  coflim  8722  coftr  8734  zorn2lem7  8963  suplem1pr  9508  axpre-sup  9624  climbdd  13790  filufint  20990  cvati  28075  atcvat4i  28106  mdsymlem2  28113  mdsymlem3  28114  sumdmdii  28124  iccllyscon  30023  dftrpred3g  30524  incsequz2  32124  lcvat  32642  hlrelat3  33023  cvrval3  33024  cvrval4N  33025  2atlt  33050  cvrat4  33054  atbtwnexOLDN  33058  atbtwnex  33059  athgt  33067  2llnmat  33135  lnjatN  33391  2lnat  33395  cdlemb  33405  lhpexle3lem  33622  cdlemf1  34174  cdlemf2  34175  cdlemf  34176  cdlemk26b-3  34518  dvh4dimlem  35057  upbdrech  37598  limcperiod  37794  cncfshift  37837  cncfperiod  37842