Theorem rexlimd 3026

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

Syntax hints:   -> wi 4   F/wnf 1708   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-ral 2917  df-rex 2918

This theorem is referenced by:  r19.29af2  3075  reusv2lem2  4869  reusv2lem2OLD  4870  ralxfrALT  4887  fvmptt  6300  ffnfv  6388  peano5  7089  tz7.49  7540  nneneq  8143  ac6sfi  8204  ixpiunwdom  8496  r1val1  8649  rankuni2b  8716  infpssrlem4  9128  zorn2lem4  9321  zorn2lem5  9322  konigthlem  9390  tskuni  9605  gruiin  9632  lbzbi  11776  reuccats1  13480  fprodle  14727  iunconnlem  21230  ptbasfi  21384  alexsubALTlem3  21853  ovoliunnul  23275  iunmbl2  23325  mptelee  25775  atom1d  29212  elabreximd  29348  iundisjf  29402  esumc  30113  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  heicant  33444  indexa  33528  sdclem2  33538  glbconxN  34664  cdleme26ee  35648  cdleme32d  35732  cdleme32f  35734  cdlemk38  36203  cdlemk19x  36231  cdlemk11t  36234  refsumcn  39189  eliuniin2  39303  rexlimd3  39335  suprnmpt  39355  dffo3f  39364  wessf1ornlem  39371  disjf1o  39378  disjinfi  39380  funimassd  39431  rnmptlb  39453  rnmptbddlem  39455  fvelimad  39458  rnmptbd2lem  39463  infnsuprnmpt  39465  upbdrech  39519  ssfiunibd  39523  iuneqfzuzlem  39550  infrpge  39567  xrralrecnnle  39602  supxrleubrnmpt  39632  infleinf2  39641  suprleubrnmpt  39649  infrnmptle  39650  infxrunb3rnmpt  39655  infxrgelbrnmpt  39683  iccshift  39744  iooshift  39748  fmul01lt1  39818  islptre  39851  rexlim2d  39857  limcperiod  39860  islpcn  39871  limclner  39883  fnlimfvre  39906  climinf2lem  39938  limsupmnflem  39952  limsupre3uzlem  39967  climuzlem  39975  dvnprodlem1  40161  dvnprodlem2  40162  itgperiod  40197  stoweidlem29  40246  stoweidlem31  40248  stoweidlem59  40276  stirlinglem13  40303  fourierdlem48  40371  fourierdlem51  40374  fourierdlem53  40376  fourierdlem80  40403  fourierdlem81  40404  fourierdlem93  40416  elaa2  40451  salexct  40552  sge00  40593  sge0f1o  40599  sge0gerp  40612  sge0lefi  40615  sge0ltfirp  40617  sge0resplit  40623  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0isum  40644  sge0xp  40646  sge0reuz  40664  sge0reuzb  40665  iundjiun  40677  voliunsge0lem  40689  meaiininc2  40702  isomenndlem  40744  ovncvrrp  40778  ovnsubaddlem1  40784  hoidmvval0  40801  hoidmvlelem1  40809  vonioo  40896  vonicc  40899  smfaddlem1  40971  smfresal  40995  smfpimbor1lem2  41006  smflimmpt  41016  smfinflem  41023  smflimsuplem7  41032  smflimsuplem8  41033  smflimsupmpt  41035  smfliminfmpt  41038  ffnafv  41251  iccpartdisj  41373  mogoldbb  41673  2zrngagrp  41943  iunord  42422