Theorem rexlimd 2866

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

Syntax hints:   -> wi 4   F/wnf 1675   e. wcel 1904   E.wrex 2757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-ral 2761  df-rex 2762

This theorem is referenced by:  r19.29af2  2915  reusv2lem2  4603  ralxfrALT  4619  fvmptt  5980  ffnfv  6064  peano5  6735  tz7.49  7180  nneneq  7773  ac6sfi  7833  ixpiunwdom  8124  r1val1  8275  rankuni2b  8342  infpssrlem4  8754  zorn2lem4  8947  zorn2lem5  8948  konigthlem  9011  tskuni  9226  gruiin  9253  lbzbi  11275  fprodle  14127  iunconlem  20519  ptbasfi  20673  alexsubALTlem3  21142  ovoliunnul  22538  iunmbl2  22589  mptelee  25004  atom1d  28087  elabreximd  28223  iundisjf  28276  esumc  28946  poimirlem24  32028  poimirlem26  32030  poimirlem27  32031  heicant  32039  indexa  32124  sdclem2  32135  glbconxN  33014  cdleme26ee  33998  cdleme32d  34082  cdleme32f  34084  cdlemk38  34553  cdlemk19x  34581  cdlemk11t  34584  refsumcn  37414  suprnmpt  37512  dffo3f  37521  wessf1ornlem  37530  disjf1o  37537  disjinfi  37539  upbdrech  37611  ssfiunibd  37615  iuneqfzuzlem  37644  infrpge  37661  iccshift  37715  iooshift  37719  fmul01lt1  37761  islptre  37796  rexlim2d  37802  limcperiod  37805  islpcn  37816  limclner  37829  dvnprodlem1  37918  dvnprodlem2  37919  itgperiod  37955  stoweidlem29  38001  stoweidlem29OLD  38002  stoweidlem31  38004  stoweidlem59  38032  stirlinglem13  38060  fourierdlem48  38130  fourierdlem51  38133  fourierdlem53  38135  fourierdlem80  38162  fourierdlem81  38163  fourierdlem93  38175  elaa2  38211  salexct  38305  sge00  38332  sge0f1o  38338  sge0gerp  38351  sge0lefi  38354  sge0ltfirp  38356  sge0resplit  38362  sge0iunmptlemre  38371  sge0iunmpt  38374  sge0isum  38383  sge0xp  38385  iundjiun  38414  voliunsge0lem  38426  isomenndlem  38470  ovncvrrp  38504  ovnsubaddlem1  38510  hoidmvval0  38527  hoidmvlelem1  38535  ffnafv  38818  iccpartdisj  38896  2zrngagrp  40451