Theorem rexlimd 3244

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∃wrex 3053

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 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3045  df-rex 3054

This theorem is referenced by:  r19.29af2  3245  iuneqconst  4967  reusv2lem2  5354  ralxfrALT  5370  funimassd  6927  fvelimad  6928  fvmptt  6988  dffo3f  7078  ffnfv  7091  frpoins3xpg  8119  frpoins3xp3g  8120  tz7.49  8413  nneneq  9170  ac6sfi  9231  ixpiunwdom  9543  r1val1  9739  rankuni2b  9806  infpssrlem4  10259  zorn2lem4  10452  zorn2lem5  10453  konigthlem  10521  tskuni  10736  gruiin  10763  lbzbi  12895  reuccatpfxs1  14712  iunconnlem  23314  ptbasfi  23468  alexsubALTlem3  23936  ovoliunnul  25408  iunmbl2  25458  mptelee  28822  atom1d  32282  elabreximd  32439  iundisjf  32518  esumc  34041  fvineqsneu  37399  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  heicant  37649  indexa  37727  sdclem2  37736  glbconxN  39372  cdleme26ee  40354  cdleme32d  40438  cdleme32f  40440  cdlemk38  40909  cdlemk19x  40937  cdlemk11t  40940  unielss  43207  oaun3lem1  43363  refsumcn  45024  eliuniin2  45114  rexlimd3  45138  suprnmpt  45168  disjf1o  45185  disjinfi  45186  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  infnsuprnmpt  45244  upbdrech  45303  ssfiunibd  45307  iuneqfzuzlem  45330  infrpge  45347  xrralrecnnle  45379  supxrleubrnmpt  45402  infleinf2  45410  suprleubrnmpt  45418  infrnmptle  45419  infxrunb3rnmpt  45424  infxrgelbrnmpt  45450  iccshift  45516  iooshift  45520  fmul01lt1  45584  islptre  45617  rexlim2d  45623  limcperiod  45626  islpcn  45637  limclner  45649  fnlimfvre  45672  climinf2lem  45704  limsupmnflem  45718  limsupre3uzlem  45733  climuzlem  45741  dvnprodlem1  45944  dvnprodlem2  45945  itgperiod  45979  stoweidlem29  46027  stoweidlem31  46029  stoweidlem59  46057  stirlinglem13  46084  fourierdlem48  46152  fourierdlem51  46155  fourierdlem80  46184  fourierdlem81  46185  fourierdlem93  46197  elaa2  46232  salexct  46332  sge00  46374  sge0f1o  46380  sge0gerp  46393  sge0lefi  46396  sge0ltfirp  46398  sge0resplit  46404  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0isum  46425  sge0xp  46427  sge0reuz  46445  sge0reuzb  46446  iundjiun  46458  voliunsge0lem  46470  meaiuninc3v  46482  meaiininc2  46486  isomenndlem  46528  ovncvrrp  46562  ovnsubaddlem1  46568  hoidmvval0  46585  hoidmvlelem1  46593  vonioo  46680  vonicc  46683  smfaddlem1  46761  smfresal  46786  smfpimbor1lem2  46797  smflimmpt  46808  smfinflem  46815  smflimsuplem7  46824  smflimsuplem8  46825  smflimsupmpt  46827  smfliminfmpt  46830  ffnafv  47172  f1oresf1o2  47292  iccpartdisj  47438  mogoldbb  47786  2zrngagrp  48237  iunord  49665