Theorem rexlimd 3264

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

Syntax hints:   → wi 4  Ⅎwnf 1780   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-ral 3060  df-rex 3069

This theorem is referenced by:  r19.29af2  3265  iuneqconst  5008  reusv2lem2  5405  ralxfrALT  5421  funimassd  6975  fvelimad  6976  fvmptt  7036  dffo3f  7126  ffnfv  7139  frpoins3xpg  8164  frpoins3xp3g  8165  tz7.49  8484  nneneq  9244  nneneqOLD  9256  ac6sfi  9318  ixpiunwdom  9628  r1val1  9824  rankuni2b  9891  infpssrlem4  10344  zorn2lem4  10537  zorn2lem5  10538  konigthlem  10606  tskuni  10821  gruiin  10848  lbzbi  12976  reuccatpfxs1  14782  iunconnlem  23451  ptbasfi  23605  alexsubALTlem3  24073  ovoliunnul  25556  iunmbl2  25606  mptelee  28925  atom1d  32382  elabreximd  32538  iundisjf  32609  esumc  34032  fvineqsneu  37394  poimirlem24  37631  poimirlem26  37633  poimirlem27  37634  heicant  37642  indexa  37720  sdclem2  37729  glbconxN  39361  cdleme26ee  40343  cdleme32d  40427  cdleme32f  40429  cdlemk38  40898  cdlemk19x  40926  cdlemk11t  40929  unielss  43207  oaun3lem1  43364  refsumcn  44968  eliuniin2  45060  rexlimd3  45084  suprnmpt  45117  disjf1o  45134  disjinfi  45135  rnmptlb  45188  rnmptbddlem  45189  rnmptbd2lem  45193  infnsuprnmpt  45195  upbdrech  45256  ssfiunibd  45260  iuneqfzuzlem  45284  infrpge  45301  xrralrecnnle  45333  supxrleubrnmpt  45356  infleinf2  45364  suprleubrnmpt  45372  infrnmptle  45373  infxrunb3rnmpt  45378  infxrgelbrnmpt  45404  iccshift  45471  iooshift  45475  fmul01lt1  45542  islptre  45575  rexlim2d  45581  limcperiod  45584  islpcn  45595  limclner  45607  fnlimfvre  45630  climinf2lem  45662  limsupmnflem  45676  limsupre3uzlem  45691  climuzlem  45699  dvnprodlem1  45902  dvnprodlem2  45903  itgperiod  45937  stoweidlem29  45985  stoweidlem31  45987  stoweidlem59  46015  stirlinglem13  46042  fourierdlem48  46110  fourierdlem51  46113  fourierdlem80  46142  fourierdlem81  46143  fourierdlem93  46155  elaa2  46190  salexct  46290  sge00  46332  sge0f1o  46338  sge0gerp  46351  sge0lefi  46354  sge0ltfirp  46356  sge0resplit  46362  sge0iunmptlemre  46371  sge0iunmpt  46374  sge0isum  46383  sge0xp  46385  sge0reuz  46403  sge0reuzb  46404  iundjiun  46416  voliunsge0lem  46428  meaiuninc3v  46440  meaiininc2  46444  isomenndlem  46486  ovncvrrp  46520  ovnsubaddlem1  46526  hoidmvval0  46543  hoidmvlelem1  46551  vonioo  46638  vonicc  46641  smfaddlem1  46719  smfresal  46744  smfpimbor1lem2  46755  smflimmpt  46766  smfinflem  46773  smflimsuplem7  46782  smflimsuplem8  46783  smflimsupmpt  46785  smfliminfmpt  46788  ffnafv  47121  f1oresf1o2  47241  iccpartdisj  47362  mogoldbb  47710  2zrngagrp  48093  iunord  48907