Theorem rexlimd 3317

Description: Deduction form of rexlimd 3317. (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 3316	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-ral 3143  df-rex 3144

This theorem is referenced by:  r19.29af2  3330  iuneqconst  4916  reusv2lem2  5286  ralxfrALT  5302  fvelimad  6718  fvmptt  6774  ffnfv  6868  peano5  7591  tz7.49  8067  nneneq  8686  ac6sfi  8748  ixpiunwdom  9041  r1val1  9201  rankuni2b  9268  infpssrlem4  9714  zorn2lem4  9907  zorn2lem5  9908  konigthlem  9976  tskuni  10191  gruiin  10218  lbzbi  12323  reuccatpfxs1  14094  iunconnlem  22018  ptbasfi  22172  alexsubALTlem3  22640  ovoliunnul  24091  iunmbl2  24141  mptelee  26667  atom1d  30114  elabreximd  30255  iundisjf  30325  esumc  31317  fvineqsneu  34708  poimirlem24  34950  poimirlem26  34952  poimirlem27  34953  heicant  34961  indexa  35040  sdclem2  35049  glbconxN  36546  cdleme26ee  37528  cdleme32d  37612  cdleme32f  37614  cdlemk38  38083  cdlemk19x  38111  cdlemk11t  38114  refsumcn  41377  eliuniin2  41476  rexlimd3  41503  suprnmpt  41520  disjf1o  41542  disjinfi  41544  funimassd  41587  rnmptlb  41604  rnmptbddlem  41605  rnmptbd2lem  41610  infnsuprnmpt  41612  upbdrech  41662  ssfiunibd  41666  iuneqfzuzlem  41692  infrpge  41709  xrralrecnnle  41743  supxrleubrnmpt  41769  infleinf2  41778  suprleubrnmpt  41786  infrnmptle  41787  infxrunb3rnmpt  41792  infxrgelbrnmpt  41820  iccshift  41884  iooshift  41888  fmul01lt1  41957  islptre  41990  rexlim2d  41996  limcperiod  41999  islpcn  42010  limclner  42022  fnlimfvre  42045  climinf2lem  42077  limsupmnflem  42091  limsupre3uzlem  42106  climuzlem  42114  dvnprodlem1  42321  dvnprodlem2  42322  itgperiod  42356  stoweidlem29  42404  stoweidlem31  42406  stoweidlem59  42434  stirlinglem13  42461  fourierdlem48  42529  fourierdlem51  42532  fourierdlem53  42534  fourierdlem80  42561  fourierdlem81  42562  fourierdlem93  42574  elaa2  42609  salexct  42707  sge00  42748  sge0f1o  42754  sge0gerp  42767  sge0lefi  42770  sge0ltfirp  42772  sge0resplit  42778  sge0iunmptlemre  42787  sge0iunmpt  42790  sge0isum  42799  sge0xp  42801  sge0reuz  42819  sge0reuzb  42820  iundjiun  42832  voliunsge0lem  42844  meaiuninc3v  42856  meaiininc2  42860  isomenndlem  42902  ovncvrrp  42936  ovnsubaddlem1  42942  hoidmvval0  42959  hoidmvlelem1  42967  vonioo  43054  vonicc  43057  smfaddlem1  43129  smfresal  43153  smfpimbor1lem2  43164  smflimmpt  43174  smfinflem  43181  smflimsuplem7  43190  smflimsuplem8  43191  smflimsupmpt  43193  smfliminfmpt  43196  ffnafv  43460  f1oresf1o2  43580  iccpartdisj  43687  mogoldbb  44035  2zrngagrp  44299  iunord  44864