Theorem rexlimd 2870

Description: Deduction form of rexlimd 2870. (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 2869	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   F/wnf 1666   e. wcel 1886   E.wrex 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-12 1932

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-nf 1667  df-ral 2741  df-rex 2742

This theorem is referenced by:  rexlimdvOLD  2877  r19.29af2  2927  reusv2lem2  4604  ralxfrALT  4618  fvmptt  5963  ffnfv  6047  peano5  6713  tz7.49  7159  nneneq  7752  ac6sfi  7812  ixpiunwdom  8103  r1val1  8254  rankuni2b  8321  infpssrlem4  8733  zorn2lem4  8926  zorn2lem5  8927  konigthlem  8990  tskuni  9205  gruiin  9232  lbzbi  11249  fprodle  14043  iunconlem  20435  ptbasfi  20589  alexsubALTlem3  21057  ovoliunnul  22453  iunmbl2  22503  mptelee  24918  atom1d  27999  elabreximd  28137  iundisjf  28192  esumc  28865  poimirlem24  31957  poimirlem26  31959  poimirlem27  31960  heicant  31968  indexa  32053  sdclem2  32064  glbconxN  32937  cdleme26ee  33921  cdleme32d  34005  cdleme32f  34007  cdlemk38  34476  cdlemk19x  34504  cdlemk11t  34507  refsumcn  37345  suprnmpt  37433  dffo3f  37444  wessf1ornlem  37453  disjf1o  37460  disjinfi  37462  upbdrech  37517  ssfiunibd  37521  iuneqfzuzlem  37551  infrpge  37568  iccshift  37613  iooshift  37617  fmul01lt1  37658  islptre  37693  rexlim2d  37699  limcperiod  37702  islpcn  37713  limclner  37726  dvnprodlem1  37815  dvnprodlem2  37816  itgperiod  37852  stoweidlem29  37883  stoweidlem29OLD  37884  stoweidlem31  37886  stoweidlem59  37914  stirlinglem13  37942  fourierdlem48  38012  fourierdlem51  38015  fourierdlem53  38017  fourierdlem80  38044  fourierdlem81  38045  fourierdlem93  38057  elaa2  38093  salexct  38187  sge00  38212  sge0f1o  38218  sge0gerp  38231  sge0lefi  38234  sge0ltfirp  38236  sge0resplit  38242  sge0iunmptlemre  38251  sge0iunmpt  38254  sge0isum  38263  sge0xp  38265  iundjiun  38292  isomenndlem  38345  ovncvrrp  38380  ovnsubaddlem1  38386  hoidmvval0  38403  hoidmvlelem1  38411  ffnafv  38667  iccpartdisj  38745  2zrngagrp  39930