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  5009  reusv2lem2  5398  ralxfrALT  5414  funimassd  6959  fvelimad  6960  fvmptt  7019  ffnfv  7118  peano5OLD  7885  frpoins3xpg  8126  frpoins3xp3g  8127  tz7.49  8445  nneneq  9209  nneneqOLD  9221  ac6sfi  9287  ixpiunwdom  9585  r1val1  9781  rankuni2b  9848  infpssrlem4  10301  zorn2lem4  10494  zorn2lem5  10495  konigthlem  10563  tskuni  10778  gruiin  10805  lbzbi  12920  reuccatpfxs1  14697  iunconnlem  22931  ptbasfi  23085  alexsubALTlem3  23553  ovoliunnul  25024  iunmbl2  25074  mptelee  28184  atom1d  31637  elabreximd  31778  iundisjf  31851  esumc  33080  fvineqsneu  36340  poimirlem24  36560  poimirlem26  36562  poimirlem27  36563  heicant  36571  indexa  36649  sdclem2  36658  glbconxN  38297  cdleme26ee  39279  cdleme32d  39363  cdleme32f  39365  cdlemk38  39834  cdlemk19x  39862  cdlemk11t  39865  unielss  42015  oaun3lem1  42172  refsumcn  43762  eliuniin2  43857  rexlimd3  43881  suprnmpt  43918  disjf1o  43937  disjinfi  43939  rnmptlb  43995  rnmptbddlem  43996  rnmptbd2lem  44000  infnsuprnmpt  44002  upbdrech  44063  ssfiunibd  44067  iuneqfzuzlem  44092  infrpge  44109  xrralrecnnle  44141  supxrleubrnmpt  44164  infleinf2  44172  suprleubrnmpt  44180  infrnmptle  44181  infxrunb3rnmpt  44186  infxrgelbrnmpt  44212  iccshift  44279  iooshift  44283  fmul01lt1  44350  islptre  44383  rexlim2d  44389  limcperiod  44392  islpcn  44403  limclner  44415  fnlimfvre  44438  climinf2lem  44470  limsupmnflem  44484  limsupre3uzlem  44499  climuzlem  44507  dvnprodlem1  44710  dvnprodlem2  44711  itgperiod  44745  stoweidlem29  44793  stoweidlem31  44795  stoweidlem59  44823  stirlinglem13  44850  fourierdlem48  44918  fourierdlem51  44921  fourierdlem80  44950  fourierdlem81  44951  fourierdlem93  44963  elaa2  44998  salexct  45098  sge00  45140  sge0f1o  45146  sge0gerp  45159  sge0lefi  45162  sge0ltfirp  45164  sge0resplit  45170  sge0iunmptlemre  45179  sge0iunmpt  45182  sge0isum  45191  sge0xp  45193  sge0reuz  45211  sge0reuzb  45212  iundjiun  45224  voliunsge0lem  45236  meaiuninc3v  45248  meaiininc2  45252  isomenndlem  45294  ovncvrrp  45328  ovnsubaddlem1  45334  hoidmvval0  45351  hoidmvlelem1  45359  vonioo  45446  vonicc  45449  smfaddlem1  45527  smfresal  45552  smfpimbor1lem2  45563  smflimmpt  45574  smfinflem  45581  smflimsuplem7  45590  smflimsuplem8  45591  smflimsupmpt  45593  smfliminfmpt  45596  ffnafv  45927  f1oresf1o2  46047  iccpartdisj  46153  mogoldbb  46501  2zrngagrp  46889  iunord  47769