Theorem rexlimd 3264

Description: Deduction form of rexlimd 3264. For a version based on fewer axioms see rexlimdv 3154. (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	⊢ Ⅎ𝑥𝜑
rexlimd.2	⊢ Ⅎ𝑥𝜒
rexlimd.3	⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimd	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Proof of Theorem rexlimd

Step	Hyp	Ref	Expression
1		rexlimd.1	. 2 ⊢ Ⅎ𝑥𝜑
2		rexlimd.2	. . 3 ⊢ Ⅎ𝑥𝜒
3	2	a1i 11	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
4		rexlimd.3	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
5	1, 3, 4	rexlimd2 3263	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1786   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-ral 3063  df-rex 3072

This theorem is referenced by:  r19.29af2  3265  iuneqconst  5009  reusv2lem2  5398  ralxfrALT  5414  funimassd  6959  fvelimad  6960  fvmptt  7019  ffnfv  7118  peano5OLD  7885  frpoins3xpg  8126  frpoins3xp3g  8127  tz7.49  8445  nneneq  9209  nneneqOLD  9221  ac6sfi  9287  ixpiunwdom  9585  r1val1  9781  rankuni2b  9848  infpssrlem4  10301  zorn2lem4  10494  zorn2lem5  10495  konigthlem  10563  tskuni  10778  gruiin  10805  lbzbi  12920  reuccatpfxs1  14697  iunconnlem  22931  ptbasfi  23085  alexsubALTlem3  23553  ovoliunnul  25024  iunmbl2  25074  mptelee  28153  atom1d  31606  elabreximd  31747  iundisjf  31820  esumc  33049  fvineqsneu  36292  poimirlem24  36512  poimirlem26  36514  poimirlem27  36515  heicant  36523  indexa  36601  sdclem2  36610  glbconxN  38249  cdleme26ee  39231  cdleme32d  39315  cdleme32f  39317  cdlemk38  39786  cdlemk19x  39814  cdlemk11t  39817  unielss  41967  oaun3lem1  42124  refsumcn  43714  eliuniin2  43809  rexlimd3  43833  suprnmpt  43870  disjf1o  43889  disjinfi  43891  rnmptlb  43947  rnmptbddlem  43948  rnmptbd2lem  43952  infnsuprnmpt  43954  upbdrech  44015  ssfiunibd  44019  iuneqfzuzlem  44044  infrpge  44061  xrralrecnnle  44093  supxrleubrnmpt  44116  infleinf2  44124  suprleubrnmpt  44132  infrnmptle  44133  infxrunb3rnmpt  44138  infxrgelbrnmpt  44164  iccshift  44231  iooshift  44235  fmul01lt1  44302  islptre  44335  rexlim2d  44341  limcperiod  44344  islpcn  44355  limclner  44367  fnlimfvre  44390  climinf2lem  44422  limsupmnflem  44436  limsupre3uzlem  44451  climuzlem  44459  dvnprodlem1  44662  dvnprodlem2  44663  itgperiod  44697  stoweidlem29  44745  stoweidlem31  44747  stoweidlem59  44775  stirlinglem13  44802  fourierdlem48  44870  fourierdlem51  44873  fourierdlem80  44902  fourierdlem81  44903  fourierdlem93  44915  elaa2  44950  salexct  45050  sge00  45092  sge0f1o  45098  sge0gerp  45111  sge0lefi  45114  sge0ltfirp  45116  sge0resplit  45122  sge0iunmptlemre  45131  sge0iunmpt  45134  sge0isum  45143  sge0xp  45145  sge0reuz  45163  sge0reuzb  45164  iundjiun  45176  voliunsge0lem  45188  meaiuninc3v  45200  meaiininc2  45204  isomenndlem  45246  ovncvrrp  45280  ovnsubaddlem1  45286  hoidmvval0  45303  hoidmvlelem1  45311  vonioo  45398  vonicc  45401  smfaddlem1  45479  smfresal  45504  smfpimbor1lem2  45515  smflimmpt  45526  smfinflem  45533  smflimsuplem7  45542  smflimsuplem8  45543  smflimsupmpt  45545  smfliminfmpt  45548  ffnafv  45879  f1oresf1o2  45999  iccpartdisj  46105  mogoldbb  46453  2zrngagrp  46841  iunord  47721