Theorem rexlimd 3264

Description: Deduction form of rexlimd 3264. For a version based on fewer axioms see rexlimdv 3154. (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 1786   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

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

This theorem is referenced by:  r19.29af2  3265  iuneqconst  5006  reusv2lem2  5395  ralxfrALT  5411  fvelimad  6954  fvmptt  7013  ffnfv  7112  peano5OLD  7879  frpoins3xpg  8120  frpoins3xp3g  8121  tz7.49  8439  nneneq  9204  nneneqOLD  9216  ac6sfi  9282  ixpiunwdom  9580  r1val1  9776  rankuni2b  9843  infpssrlem4  10296  zorn2lem4  10489  zorn2lem5  10490  konigthlem  10558  tskuni  10773  gruiin  10800  lbzbi  12915  reuccatpfxs1  14692  iunconnlem  22912  ptbasfi  23066  alexsubALTlem3  23534  ovoliunnul  25005  iunmbl2  25055  mptelee  28132  atom1d  31583  elabreximd  31724  iundisjf  31797  esumc  32986  fvineqsneu  36229  poimirlem24  36449  poimirlem26  36451  poimirlem27  36452  heicant  36460  indexa  36538  sdclem2  36547  glbconxN  38186  cdleme26ee  39168  cdleme32d  39252  cdleme32f  39254  cdlemk38  39723  cdlemk19x  39751  cdlemk11t  39754  unielss  41899  oaun3lem1  42056  refsumcn  43646  eliuniin2  43741  rexlimd3  43765  suprnmpt  43802  disjf1o  43821  disjinfi  43823  funimassd  43862  rnmptlb  43880  rnmptbddlem  43881  rnmptbd2lem  43886  infnsuprnmpt  43888  upbdrech  43949  ssfiunibd  43953  iuneqfzuzlem  43978  infrpge  43995  xrralrecnnle  44027  supxrleubrnmpt  44050  infleinf2  44058  suprleubrnmpt  44066  infrnmptle  44067  infxrunb3rnmpt  44072  infxrgelbrnmpt  44098  iccshift  44165  iooshift  44169  fmul01lt1  44236  islptre  44269  rexlim2d  44275  limcperiod  44278  islpcn  44289  limclner  44301  fnlimfvre  44324  climinf2lem  44356  limsupmnflem  44370  limsupre3uzlem  44385  climuzlem  44393  dvnprodlem1  44596  dvnprodlem2  44597  itgperiod  44631  stoweidlem29  44679  stoweidlem31  44681  stoweidlem59  44709  stirlinglem13  44736  fourierdlem48  44804  fourierdlem51  44807  fourierdlem80  44836  fourierdlem81  44837  fourierdlem93  44849  elaa2  44884  salexct  44984  sge00  45026  sge0f1o  45032  sge0gerp  45045  sge0lefi  45048  sge0ltfirp  45050  sge0resplit  45056  sge0iunmptlemre  45065  sge0iunmpt  45068  sge0isum  45077  sge0xp  45079  sge0reuz  45097  sge0reuzb  45098  iundjiun  45110  voliunsge0lem  45122  meaiuninc3v  45134  meaiininc2  45138  isomenndlem  45180  ovncvrrp  45214  ovnsubaddlem1  45220  hoidmvval0  45237  hoidmvlelem1  45245  vonioo  45332  vonicc  45335  smfaddlem1  45413  smfresal  45438  smfpimbor1lem2  45449  smflimmpt  45460  smfinflem  45467  smflimsuplem7  45476  smflimsuplem8  45477  smflimsupmpt  45479  smfliminfmpt  45482  ffnafv  45813  f1oresf1o2  45933  iccpartdisj  46039  mogoldbb  46387  2zrngagrp  46742  iunord  47622