Theorem rexlimd 3247

Description: Deduction form of rexlimd 3247. (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 3246	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1789   ∈ wcel 2109  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-nf 1790  df-ral 3070  df-rex 3071

This theorem is referenced by:  r19.29af2  3260  iuneqconst  4940  reusv2lem2  5325  ralxfrALT  5341  fvelimad  6830  fvmptt  6889  ffnfv  6986  peano5OLD  7728  tz7.49  8260  nneneq  8956  nneneqOLD  8969  ac6sfi  9019  ixpiunwdom  9310  r1val1  9528  rankuni2b  9595  infpssrlem4  10046  zorn2lem4  10239  zorn2lem5  10240  konigthlem  10308  tskuni  10523  gruiin  10550  lbzbi  12658  reuccatpfxs1  14441  iunconnlem  22559  ptbasfi  22713  alexsubALTlem3  23181  ovoliunnul  24652  iunmbl2  24702  mptelee  27244  atom1d  30694  elabreximd  30834  iundisjf  30907  esumc  31998  frpoins3xpg  33766  frpoins3xp3g  33767  fvineqsneu  35561  poimirlem24  35780  poimirlem26  35782  poimirlem27  35783  heicant  35791  indexa  35870  sdclem2  35879  glbconxN  37371  cdleme26ee  38353  cdleme32d  38437  cdleme32f  38439  cdlemk38  38908  cdlemk19x  38936  cdlemk11t  38939  refsumcn  42526  eliuniin2  42622  rexlimd3  42646  suprnmpt  42663  disjf1o  42682  disjinfi  42684  funimassd  42723  rnmptlb  42741  rnmptbddlem  42742  rnmptbd2lem  42747  infnsuprnmpt  42749  upbdrech  42798  ssfiunibd  42802  iuneqfzuzlem  42827  infrpge  42844  xrralrecnnle  42876  supxrleubrnmpt  42900  infleinf2  42908  suprleubrnmpt  42916  infrnmptle  42917  infxrunb3rnmpt  42922  infxrgelbrnmpt  42948  iccshift  43010  iooshift  43014  fmul01lt1  43081  islptre  43114  rexlim2d  43120  limcperiod  43123  islpcn  43134  limclner  43146  fnlimfvre  43169  climinf2lem  43201  limsupmnflem  43215  limsupre3uzlem  43230  climuzlem  43238  dvnprodlem1  43441  dvnprodlem2  43442  itgperiod  43476  stoweidlem29  43524  stoweidlem31  43526  stoweidlem59  43554  stirlinglem13  43581  fourierdlem48  43649  fourierdlem51  43652  fourierdlem80  43681  fourierdlem81  43682  fourierdlem93  43694  elaa2  43729  salexct  43827  sge00  43868  sge0f1o  43874  sge0gerp  43887  sge0lefi  43890  sge0ltfirp  43892  sge0resplit  43898  sge0iunmptlemre  43907  sge0iunmpt  43910  sge0isum  43919  sge0xp  43921  sge0reuz  43939  sge0reuzb  43940  iundjiun  43952  voliunsge0lem  43964  meaiuninc3v  43976  meaiininc2  43980  isomenndlem  44022  ovncvrrp  44056  ovnsubaddlem1  44062  hoidmvval0  44079  hoidmvlelem1  44087  vonioo  44174  vonicc  44177  smfaddlem1  44249  smfresal  44273  smfpimbor1lem2  44284  smflimmpt  44294  smfinflem  44301  smflimsuplem7  44310  smflimsuplem8  44311  smflimsupmpt  44313  smfliminfmpt  44316  ffnafv  44614  f1oresf1o2  44734  iccpartdisj  44841  mogoldbb  45189  2zrngagrp  45453  iunord  46334