Theorem rexlimd 3243

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2113  ∃wrex 3060

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 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3052  df-rex 3061

This theorem is referenced by:  r19.29af2  3244  iuneqconst  4958  reusv2lem2  5344  ralxfrALT  5360  funimassd  6900  fvelimad  6901  fvmptt  6961  dffo3f  7051  ffnfv  7064  frpoins3xpg  8082  frpoins3xp3g  8083  tz7.49  8376  nneneq  9130  ac6sfi  9184  ixpiunwdom  9495  r1val1  9698  rankuni2b  9765  infpssrlem4  10216  zorn2lem4  10409  zorn2lem5  10410  konigthlem  10479  tskuni  10694  gruiin  10721  lbzbi  12849  reuccatpfxs1  14670  iunconnlem  23371  ptbasfi  23525  alexsubALTlem3  23993  ovoliunnul  25464  iunmbl2  25514  mpteleeOLD  28968  atom1d  32428  elabreximd  32585  iundisjf  32664  esumc  34208  fvineqsneu  37612  poimirlem24  37841  poimirlem26  37843  poimirlem27  37844  heicant  37852  indexa  37930  sdclem2  37939  glbconxN  39634  cdleme26ee  40616  cdleme32d  40700  cdleme32f  40702  cdlemk38  41171  cdlemk19x  41199  cdlemk11t  41202  unielss  43456  oaun3lem1  43612  refsumcn  45271  eliuniin2  45360  rexlimd3  45384  suprnmpt  45414  disjf1o  45431  disjinfi  45432  rnmptlb  45483  rnmptbddlem  45484  rnmptbd2lem  45488  infnsuprnmpt  45490  upbdrech  45549  ssfiunibd  45553  iuneqfzuzlem  45575  infrpge  45592  xrralrecnnle  45623  supxrleubrnmpt  45646  infleinf2  45654  suprleubrnmpt  45662  infrnmptle  45663  infxrunb3rnmpt  45668  infxrgelbrnmpt  45694  iccshift  45760  iooshift  45764  fmul01lt1  45828  islptre  45861  rexlim2d  45867  limcperiod  45870  islpcn  45879  limclner  45891  fnlimfvre  45914  climinf2lem  45946  limsupmnflem  45960  limsupre3uzlem  45975  climuzlem  45983  dvnprodlem1  46186  dvnprodlem2  46187  itgperiod  46221  stoweidlem29  46269  stoweidlem31  46271  stoweidlem59  46299  stirlinglem13  46326  fourierdlem48  46394  fourierdlem51  46397  fourierdlem80  46426  fourierdlem81  46427  fourierdlem93  46439  elaa2  46474  salexct  46574  sge00  46616  sge0f1o  46622  sge0gerp  46635  sge0lefi  46638  sge0ltfirp  46640  sge0resplit  46646  sge0iunmptlemre  46655  sge0iunmpt  46658  sge0isum  46667  sge0xp  46669  sge0reuz  46687  sge0reuzb  46688  iundjiun  46700  voliunsge0lem  46712  meaiuninc3v  46724  meaiininc2  46728  isomenndlem  46770  ovncvrrp  46804  ovnsubaddlem1  46810  hoidmvval0  46827  hoidmvlelem1  46835  vonioo  46922  vonicc  46925  smfaddlem1  47003  smfresal  47028  smfpimbor1lem2  47039  smflimmpt  47050  smfinflem  47057  smflimsuplem7  47066  smflimsuplem8  47067  smflimsupmpt  47069  smfliminfmpt  47072  ffnafv  47413  f1oresf1o2  47533  iccpartdisj  47679  mogoldbb  48027  2zrngagrp  48491  iunord  49917