Theorem rexlimd 3247

Description: Deduction form of rexlimd 3247. For a version based on fewer axioms see rexlimdv 3139. (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 3246	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1790   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3055  df-rex 3065

This theorem is referenced by:  r19.29af2  3248  iuneqconst  4940  reusv2lem2  5335  ralxfrALT  5351  funimassd  6900  fvelimad  6901  fvmptt  6963  dffo3f  7054  ffnfv  7067  frpoins3xpg  8087  frpoins3xp3g  8088  tz7.49  8381  nneneq  9137  ac6sfi  9191  ixpiunwdom  9502  r1val1  9708  rankuni2b  9775  infpssrlem4  10226  zorn2lem4  10419  zorn2lem5  10420  konigthlem  10489  tskuni  10704  gruiin  10731  lbzbi  12884  reuccatpfxs1  14707  iunconnlem  23417  ptbasfi  23571  alexsubALTlem3  24039  ovoliunnul  25499  iunmbl2  25549  mpteleeOLD  28989  atom1d  32449  elabreximd  32605  iundisjf  32685  esumc  34242  fvineqsneu  37780  poimirlem24  38018  poimirlem26  38020  poimirlem27  38021  heicant  38029  indexa  38107  sdclem2  38116  glbconxN  39877  cdleme26ee  40859  cdleme32d  40943  cdleme32f  40945  cdlemk38  41414  cdlemk19x  41442  cdlemk11t  41445  unielss  43670  oaun3lem1  43826  refsumcn  45485  eliuniin2  45574  rexlimd3  45598  suprnmpt  45628  disjf1o  45645  disjinfi  45646  rnmptlb  45694  rnmptbddlem  45695  rnmptbd2lem  45699  infnsuprnmpt  45701  upbdrech  45760  ssfiunibd  45764  iuneqfzuzlem  45786  infrpge  45803  xrralrecnnle  45834  supxrleubrnmpt  45856  infleinf2  45864  suprleubrnmpt  45872  infrnmptle  45873  infxrunb3rnmpt  45878  infxrgelbrnmpt  45904  iccshift  45970  iooshift  45974  fmul01lt1  46038  islptre  46071  rexlim2d  46077  limcperiod  46080  islpcn  46089  limclner  46101  fnlimfvre  46124  climinf2lem  46156  limsupmnflem  46170  limsupre3uzlem  46185  climuzlem  46193  dvnprodlem1  46396  dvnprodlem2  46397  itgperiod  46431  stoweidlem29  46479  stoweidlem31  46481  stoweidlem59  46509  stirlinglem13  46536  fourierdlem48  46604  fourierdlem51  46607  fourierdlem80  46636  fourierdlem81  46637  fourierdlem93  46649  elaa2  46684  salexct  46784  sge00  46826  sge0f1o  46832  sge0gerp  46845  sge0lefi  46848  sge0ltfirp  46850  sge0resplit  46856  sge0iunmptlemre  46865  sge0iunmpt  46868  sge0isum  46877  sge0xp  46879  sge0reuz  46897  sge0reuzb  46898  iundjiun  46910  voliunsge0lem  46922  meaiuninc3v  46934  meaiininc2  46938  isomenndlem  46980  ovncvrrp  47014  ovnsubaddlem1  47020  hoidmvval0  47037  hoidmvlelem1  47045  vonioo  47132  vonicc  47135  smfaddlem1  47213  smfresal  47238  smfpimbor1lem2  47249  smflimmpt  47260  smfinflem  47267  smflimsuplem7  47276  smflimsuplem8  47277  smflimsupmpt  47279  smfliminfmpt  47282  ffnafv  47641  f1oresf1o2  47761  iccpartdisj  47919  mogoldbb  48283  2zrngagrp  48747  iunord  50173