Theorem rexlimd 3248

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

Syntax hints:   → wi 4  Ⅎwnf 1791   ∈ wcel 2121  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-nf 1792  df-ral 3056  df-rex 3066

This theorem is referenced by:  r19.29af2  3249  iuneqconst  4936  reusv2lem2  5331  ralxfrALT  5347  funimassd  6897  fvelimad  6898  fvmptt  6960  dffo3f  7051  ffnfv  7064  frpoins3xpg  8084  frpoins3xp3g  8085  tz7.49  8378  nneneq  9134  ac6sfi  9188  ixpiunwdom  9499  r1val1  9705  rankuni2b  9772  infpssrlem4  10223  zorn2lem4  10416  zorn2lem5  10417  konigthlem  10486  tskuni  10701  gruiin  10728  lbzbi  12881  reuccatpfxs1  14704  iunconnlem  23414  ptbasfi  23568  alexsubALTlem3  24036  ovoliunnul  25496  iunmbl2  25546  mpteleeOLD  28986  atom1d  32446  elabreximd  32602  iundisjf  32682  esumc  34247  fvineqsneu  37788  poimirlem24  38026  poimirlem26  38028  poimirlem27  38029  heicant  38037  indexa  38115  sdclem2  38124  glbconxN  39885  cdleme26ee  40867  cdleme32d  40951  cdleme32f  40953  cdlemk38  41422  cdlemk19x  41450  cdlemk11t  41453  unielss  43678  oaun3lem1  43834  refsumcn  45493  eliuniin2  45581  rexlimd3  45605  suprnmpt  45635  disjf1o  45652  disjinfi  45653  rnmptlb  45701  rnmptbddlem  45702  rnmptbd2lem  45706  infnsuprnmpt  45708  upbdrech  45767  ssfiunibd  45771  iuneqfzuzlem  45793  infrpge  45810  xrralrecnnle  45841  supxrleubrnmpt  45863  infleinf2  45871  suprleubrnmpt  45879  infrnmptle  45880  infxrunb3rnmpt  45885  infxrgelbrnmpt  45911  iccshift  45977  iooshift  45981  fmul01lt1  46045  islptre  46078  rexlim2d  46084  limcperiod  46087  islpcn  46096  limclner  46108  fnlimfvre  46131  climinf2lem  46163  limsupmnflem  46177  limsupre3uzlem  46192  climuzlem  46200  dvnprodlem1  46403  dvnprodlem2  46404  itgperiod  46438  stoweidlem29  46486  stoweidlem31  46488  stoweidlem59  46516  stirlinglem13  46543  fourierdlem48  46611  fourierdlem51  46614  fourierdlem80  46643  fourierdlem81  46644  fourierdlem93  46656  elaa2  46691  salexct  46791  sge00  46833  sge0f1o  46839  sge0gerp  46852  sge0lefi  46855  sge0ltfirp  46857  sge0resplit  46863  sge0iunmptlemre  46872  sge0iunmpt  46875  sge0isum  46884  sge0xp  46886  sge0reuz  46904  sge0reuzb  46905  iundjiun  46917  voliunsge0lem  46929  meaiuninc3v  46941  meaiininc2  46945  isomenndlem  46987  ovncvrrp  47021  ovnsubaddlem1  47027  hoidmvval0  47044  hoidmvlelem1  47052  vonioo  47139  vonicc  47142  smfaddlem1  47220  smfresal  47245  smfpimbor1lem2  47256  smflimmpt  47267  smfinflem  47274  smflimsuplem7  47283  smflimsuplem8  47284  smflimsupmpt  47286  smfliminfmpt  47289  ffnafv  47648  f1oresf1o2  47768  iccpartdisj  47926  mogoldbb  48290  2zrngagrp  48754  iunord  50180