Theorem rexlimd 3268

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

Syntax hints:   → wi 4  Ⅎwnf 1802   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-ral 3076  df-rex 3086

This theorem is referenced by:  r19.29af2  3269  iuneqconst  4960  reusv2lem2  5355  ralxfrALT  5371  funimassd  6929  fvelimad  6930  fvmptt  6992  dffo3f  7083  ffnfv  7096  frpoins3xpg  8115  frpoins3xp3g  8116  tz7.49  8411  nneneq  9170  ac6sfi  9224  ixpiunwdom  9535  r1val1  9741  rankuni2b  9808  infpssrlem4  10260  zorn2lem4  10453  zorn2lem5  10454  konigthlem  10523  tskuni  10738  gruiin  10765  lbzbi  12934  reuccatpfxs1  14757  iunconnlem  23467  ptbasfi  23621  alexsubALTlem3  24089  ovoliunnul  25549  iunmbl2  25599  mpteleeOLD  29042  atom1d  32502  elabreximd  32658  iundisjf  32738  esumc  34309  fvineqsneu  37869  poimirlem24  38107  poimirlem26  38109  poimirlem27  38110  heicant  38118  indexa  38196  sdclem2  38205  glbconxN  39966  cdleme26ee  40948  cdleme32d  41032  cdleme32f  41034  cdlemk38  41503  cdlemk19x  41531  cdlemk11t  41534  unielss  43759  oaun3lem1  43915  refsumcn  45574  eliuniin2  45662  rexlimd3  45686  suprnmpt  45716  disjf1o  45733  disjinfi  45734  rnmptlb  45782  rnmptbddlem  45783  rnmptbd2lem  45787  infnsuprnmpt  45789  upbdrech  45848  ssfiunibd  45852  iuneqfzuzlem  45874  infrpge  45891  xrralrecnnle  45922  supxrleubrnmpt  45944  infleinf2  45952  suprleubrnmpt  45960  infrnmptle  45961  infxrunb3rnmpt  45966  infxrgelbrnmpt  45992  iccshift  46058  iooshift  46062  fmul01lt1  46126  islptre  46159  rexlim2d  46165  limcperiod  46168  islpcn  46177  limclner  46189  fnlimfvre  46212  climinf2lem  46244  limsupmnflem  46258  limsupre3uzlem  46273  climuzlem  46281  dvnprodlem1  46484  dvnprodlem2  46485  itgperiod  46519  stoweidlem29  46567  stoweidlem31  46569  stoweidlem59  46597  stirlinglem13  46624  fourierdlem48  46692  fourierdlem51  46695  fourierdlem80  46724  fourierdlem81  46725  fourierdlem93  46737  elaa2  46772  salexct  46872  sge00  46914  sge0f1o  46920  sge0gerp  46933  sge0lefi  46936  sge0ltfirp  46938  sge0resplit  46944  sge0iunmptlemre  46953  sge0iunmpt  46956  sge0isum  46965  sge0xp  46967  sge0reuz  46985  sge0reuzb  46986  iundjiun  46998  voliunsge0lem  47010  meaiuninc3v  47022  meaiininc2  47026  isomenndlem  47068  ovncvrrp  47102  ovnsubaddlem1  47108  hoidmvval0  47125  hoidmvlelem1  47133  vonioo  47220  vonicc  47223  smfaddlem1  47301  smfresal  47326  smfpimbor1lem2  47337  smflimmpt  47348  smfinflem  47355  smflimsuplem7  47364  smflimsuplem8  47365  smflimsupmpt  47367  smfliminfmpt  47370  ffnafv  47729  f1oresf1o2  47849  iccpartdisj  48007  mogoldbb  48371  2zrngagrp  48835  iunord  50261