Theorem rexlimd 3246

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2104  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-12 2169

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

This theorem is referenced by:  r19.29af2  3247  iuneqconst  4942  reusv2lem2  5331  ralxfrALT  5347  fvelimad  6868  fvmptt  6927  ffnfv  7024  peano5OLD  7773  tz7.49  8307  nneneq  9030  nneneqOLD  9042  ac6sfi  9102  ixpiunwdom  9393  r1val1  9588  rankuni2b  9655  infpssrlem4  10108  zorn2lem4  10301  zorn2lem5  10302  konigthlem  10370  tskuni  10585  gruiin  10612  lbzbi  12722  reuccatpfxs1  14505  iunconnlem  22623  ptbasfi  22777  alexsubALTlem3  23245  ovoliunnul  24716  iunmbl2  24766  mptelee  27308  atom1d  30760  elabreximd  30900  iundisjf  30973  esumc  32064  frpoins3xpg  33832  frpoins3xp3g  33833  fvineqsneu  35626  poimirlem24  35845  poimirlem26  35847  poimirlem27  35848  heicant  35856  indexa  35935  sdclem2  35944  glbconxN  37434  cdleme26ee  38416  cdleme32d  38500  cdleme32f  38502  cdlemk38  38971  cdlemk19x  38999  cdlemk11t  39002  refsumcn  42611  eliuniin2  42707  rexlimd3  42731  suprnmpt  42754  disjf1o  42773  disjinfi  42775  funimassd  42815  rnmptlb  42833  rnmptbddlem  42834  rnmptbd2lem  42839  infnsuprnmpt  42841  upbdrech  42892  ssfiunibd  42896  iuneqfzuzlem  42921  infrpge  42938  xrralrecnnle  42970  supxrleubrnmpt  42994  infleinf2  43002  suprleubrnmpt  43010  infrnmptle  43011  infxrunb3rnmpt  43016  infxrgelbrnmpt  43042  iccshift  43105  iooshift  43109  fmul01lt1  43176  islptre  43209  rexlim2d  43215  limcperiod  43218  islpcn  43229  limclner  43241  fnlimfvre  43264  climinf2lem  43296  limsupmnflem  43310  limsupre3uzlem  43325  climuzlem  43333  dvnprodlem1  43536  dvnprodlem2  43537  itgperiod  43571  stoweidlem29  43619  stoweidlem31  43621  stoweidlem59  43649  stirlinglem13  43676  fourierdlem48  43744  fourierdlem51  43747  fourierdlem80  43776  fourierdlem81  43777  fourierdlem93  43789  elaa2  43824  salexct  43922  sge00  43964  sge0f1o  43970  sge0gerp  43983  sge0lefi  43986  sge0ltfirp  43988  sge0resplit  43994  sge0iunmptlemre  44003  sge0iunmpt  44006  sge0isum  44015  sge0xp  44017  sge0reuz  44035  sge0reuzb  44036  iundjiun  44048  voliunsge0lem  44060  meaiuninc3v  44072  meaiininc2  44076  isomenndlem  44118  ovncvrrp  44152  ovnsubaddlem1  44158  hoidmvval0  44175  hoidmvlelem1  44183  vonioo  44270  vonicc  44273  smfaddlem1  44351  smfresal  44376  smfpimbor1lem2  44387  smflimmpt  44397  smfinflem  44404  smflimsuplem7  44413  smflimsuplem8  44414  smflimsupmpt  44416  smfliminfmpt  44419  ffnafv  44721  f1oresf1o2  44841  iccpartdisj  44947  mogoldbb  45295  2zrngagrp  45559  iunord  46440