Theorem rexlimd 3266

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2108  ∃wrex 3070

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 2007  ax-12 2177

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

This theorem is referenced by:  r19.29af2  3267  iuneqconst  5003  reusv2lem2  5399  ralxfrALT  5415  funimassd  6975  fvelimad  6976  fvmptt  7036  dffo3f  7126  ffnfv  7139  frpoins3xpg  8165  frpoins3xp3g  8166  tz7.49  8485  nneneq  9246  nneneqOLD  9258  ac6sfi  9320  ixpiunwdom  9630  r1val1  9826  rankuni2b  9893  infpssrlem4  10346  zorn2lem4  10539  zorn2lem5  10540  konigthlem  10608  tskuni  10823  gruiin  10850  lbzbi  12978  reuccatpfxs1  14785  iunconnlem  23435  ptbasfi  23589  alexsubALTlem3  24057  ovoliunnul  25542  iunmbl2  25592  mptelee  28910  atom1d  32372  elabreximd  32529  iundisjf  32602  esumc  34052  fvineqsneu  37412  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  heicant  37662  indexa  37740  sdclem2  37749  glbconxN  39380  cdleme26ee  40362  cdleme32d  40446  cdleme32f  40448  cdlemk38  40917  cdlemk19x  40945  cdlemk11t  40948  unielss  43230  oaun3lem1  43387  refsumcn  45035  eliuniin2  45125  rexlimd3  45149  suprnmpt  45179  disjf1o  45196  disjinfi  45197  rnmptlb  45250  rnmptbddlem  45251  rnmptbd2lem  45255  infnsuprnmpt  45257  upbdrech  45317  ssfiunibd  45321  iuneqfzuzlem  45345  infrpge  45362  xrralrecnnle  45394  supxrleubrnmpt  45417  infleinf2  45425  suprleubrnmpt  45433  infrnmptle  45434  infxrunb3rnmpt  45439  infxrgelbrnmpt  45465  iccshift  45531  iooshift  45535  fmul01lt1  45601  islptre  45634  rexlim2d  45640  limcperiod  45643  islpcn  45654  limclner  45666  fnlimfvre  45689  climinf2lem  45721  limsupmnflem  45735  limsupre3uzlem  45750  climuzlem  45758  dvnprodlem1  45961  dvnprodlem2  45962  itgperiod  45996  stoweidlem29  46044  stoweidlem31  46046  stoweidlem59  46074  stirlinglem13  46101  fourierdlem48  46169  fourierdlem51  46172  fourierdlem80  46201  fourierdlem81  46202  fourierdlem93  46214  elaa2  46249  salexct  46349  sge00  46391  sge0f1o  46397  sge0gerp  46410  sge0lefi  46413  sge0ltfirp  46415  sge0resplit  46421  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0isum  46442  sge0xp  46444  sge0reuz  46462  sge0reuzb  46463  iundjiun  46475  voliunsge0lem  46487  meaiuninc3v  46499  meaiininc2  46503  isomenndlem  46545  ovncvrrp  46579  ovnsubaddlem1  46585  hoidmvval0  46602  hoidmvlelem1  46610  vonioo  46697  vonicc  46700  smfaddlem1  46778  smfresal  46803  smfpimbor1lem2  46814  smflimmpt  46825  smfinflem  46832  smflimsuplem7  46841  smflimsuplem8  46842  smflimsupmpt  46844  smfliminfmpt  46847  ffnafv  47183  f1oresf1o2  47303  iccpartdisj  47424  mogoldbb  47772  2zrngagrp  48165  iunord  49195