Theorem rexlimd 3270

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3078  df-rex 3088

This theorem is used by:  r19.29af2  3271  iuneqconst  4963  reusv2lem2  5361  ralxfrALT  5377  funimassd  6943  fvelimad  6944  fvmptt  7006  dffo3f  7098  ffnfv  7111  frpoins3xpg  8141  frpoins3xp3g  8142  tz7.49  8439  nneneq  9205  ac6sfi  9259  ixpiunwdom  9568  r1val1  9776  rankuni2b  9848  infpssrlem4  10365  zorn2lem4  10558  zorn2lem5  10559  konigthlem  10634  tskuni  10849  gruiin  10876  lbzbi  13044  reuccatpfxs1  14876  iunconnlem  23725  ptbasfi  23880  alexsubALTlem3  24348  ovoliunnul  25808  iunmbl2  25858  mpteleeOLD  29455  atom1d  32937  elabreximd  33088  iundisjf  33165  esumc  34665  fvineqsneu  38302  poimirlem24  38530  poimirlem26  38532  poimirlem27  38533  heicant  38541  indexa  38635  sdclem2  38644  glbconxN  40403  cdleme26ee  41385  cdleme32d  41469  cdleme32f  41471  cdlemk38  41940  cdlemk19x  41968  cdlemk11t  41971  unielss  44178  oaun3lem1  44334  refsumcn  45990  eliuniin2  46078  rexlimd3  46102  suprnmpt  46132  disjf1o  46149  disjinfi  46150  rnmptlb  46198  rnmptbddlem  46199  rnmptbd2lem  46203  infnsuprnmpt  46205  upbdrech  46264  ssfiunibd  46268  iuneqfzuzlem  46290  infrpge  46307  xrralrecnnle  46338  supxrleubrnmpt  46360  infleinf2  46368  suprleubrnmpt  46376  infrnmptle  46377  infxrunb3rnmpt  46382  infxrgelbrnmpt  46408  iccshift  46474  iooshift  46478  fmul01lt1  46542  islptre  46575  rexlim2d  46581  limcperiod  46584  islpcn  46593  limclner  46605  fnlimfvre  46628  climinf2lem  46660  limsupmnflem  46674  limsupre3uzlem  46689  climuzlem  46697  dvnprodlem1  46900  dvnprodlem2  46901  itgperiod  46935  stoweidlem29  46983  stoweidlem31  46985  stoweidlem59  47013  stirlinglem13  47040  fourierdlem48  47108  fourierdlem51  47111  fourierdlem80  47140  fourierdlem81  47141  fourierdlem93  47153  elaa2  47188  salexct  47288  sge00  47330  sge0f1o  47336  sge0gerp  47349  sge0lefi  47352  sge0ltfirp  47354  sge0resplit  47360  sge0iunmptlemre  47369  sge0iunmpt  47372  sge0isum  47381  sge0xp  47383  sge0reuz  47401  sge0reuzb  47402  iundjiun  47414  voliunsge0lem  47426  meaiuninc3v  47438  meaiininc2  47442  isomenndlem  47484  ovncvrrp  47518  ovnsubaddlem1  47524  hoidmvval0  47541  hoidmvlelem1  47549  vonioo  47636  vonicc  47639  smfaddlem1  47717  smfresal  47742  smfpimbor1lem2  47753  smflimmpt  47764  smfinflem  47771  smflimsuplem7  47780  smflimsuplem8  47781  smflimsupmpt  47783  smfliminfmpt  47786  ffnafv  48185  f1oresf1o2  48305  iccpartdisj  48463  mogoldbb  48827  2zrngagrp  49290  iunord  50728