Theorem rexlimd 2941

Description: Deduction form of rexlimd 2941. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)

Hypotheses

Ref	Expression
rexlimd.1	|- F/ x ph
rexlimd.2	|- F/ x ch
rexlimd.3	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )

Assertion

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

Proof of Theorem rexlimd

Step	Hyp	Ref	Expression
1		rexlimd.1	. 2 |- F/ x ph
2		rexlimd.2	. . 3 |- F/ x ch
3	2	a1i 11	. 2 |- ( ph -> F/ x ch )
4		rexlimd.3	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
5	1, 3, 4	rexlimd2 2940	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   F/wnf 1617   e. wcel 1819   E.wrex 2808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-nf 1618  df-ral 2812  df-rex 2813

This theorem is referenced by:  rexlimdvOLD  2948  r19.29af2  2995  reusv2lem2  4658  reusv6OLD  4667  ralxfrALT  4675  fvmptt  5972  ffnfv  6058  peano5  6722  tz7.49  7128  nneneq  7719  ac6sfi  7782  ixpiunwdom  8035  r1val1  8221  rankuni2b  8288  infpssrlem4  8703  zorn2lem4  8896  zorn2lem5  8897  konigthlem  8960  tskuni  9178  gruiin  9205  lbzbi  11195  iunconlem  20053  ptbasfi  20207  alexsubALTlem3  20674  ovoliunnul  22043  iunmbl2  22092  mptelee  24324  atom1d  27398  elabreximd  27535  iundisjf  27585  esumc  28217  heicant  30211  indexa  30386  sdclem2  30397  refsumcn  31566  suprnmpt  31612  upbdrech  31666  ssfiunibd  31670  iccshift  31719  iooshift  31723  fmul01lt1  31741  fprodle  31765  islptre  31786  rexlim2d  31792  limcperiod  31795  islpcn  31806  limclner  31818  dvnprodlem1  31904  dvnprodlem2  31905  itgperiod  31941  stoweidlem29  31972  stoweidlem31  31974  stoweidlem59  32002  stirlinglem13  32029  fourierdlem48  32098  fourierdlem51  32101  fourierdlem53  32103  fourierdlem80  32130  fourierdlem81  32131  fourierdlem93  32143  elaa2  32178  ffnafv  32417  2zrngagrp  32851  glbconxN  35203  cdleme26ee  36187  cdleme32d  36271  cdleme32f  36273  cdlemk38  36742  cdlemk19x  36770  cdlemk11t  36773