Theorem rexlimd 3272

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

Syntax hints:   → wi 4  Ⅎwnf 1806   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-ral 3080  df-rex 3090

This theorem is referenced by:  r19.29af2  3273  iuneqconst  4964  reusv2lem2  5361  ralxfrALT  5377  funimassd  6937  fvelimad  6938  fvmptt  7000  dffo3f  7091  ffnfv  7104  frpoins3xpg  8124  frpoins3xp3g  8125  tz7.49  8420  nneneq  9178  ac6sfi  9232  ixpiunwdom  9540  r1val1  9746  rankuni2b  9813  infpssrlem4  10278  zorn2lem4  10471  zorn2lem5  10472  konigthlem  10541  tskuni  10756  gruiin  10783  lbzbi  12951  reuccatpfxs1  14774  iunconnlem  23545  ptbasfi  23699  alexsubALTlem3  24167  ovoliunnul  25627  iunmbl2  25677  mpteleeOLD  29154  atom1d  32614  elabreximd  32766  iundisjf  32844  esumc  34358  fvineqsneu  37917  poimirlem24  38155  poimirlem26  38157  poimirlem27  38158  heicant  38166  indexa  38244  sdclem2  38253  glbconxN  40014  cdleme26ee  40996  cdleme32d  41080  cdleme32f  41082  cdlemk38  41551  cdlemk19x  41579  cdlemk11t  41582  unielss  43807  oaun3lem1  43963  refsumcn  45608  eliuniin2  45696  rexlimd3  45720  suprnmpt  45750  disjf1o  45767  disjinfi  45768  rnmptlb  45816  rnmptbddlem  45817  rnmptbd2lem  45821  infnsuprnmpt  45823  upbdrech  45882  ssfiunibd  45886  iuneqfzuzlem  45908  infrpge  45925  xrralrecnnle  45956  supxrleubrnmpt  45978  infleinf2  45986  suprleubrnmpt  45994  infrnmptle  45995  infxrunb3rnmpt  46000  infxrgelbrnmpt  46026  iccshift  46092  iooshift  46096  fmul01lt1  46160  islptre  46193  rexlim2d  46199  limcperiod  46202  islpcn  46211  limclner  46223  fnlimfvre  46246  climinf2lem  46278  limsupmnflem  46292  limsupre3uzlem  46307  climuzlem  46315  dvnprodlem1  46518  dvnprodlem2  46519  itgperiod  46553  stoweidlem29  46601  stoweidlem31  46603  stoweidlem59  46631  stirlinglem13  46658  fourierdlem48  46726  fourierdlem51  46729  fourierdlem80  46758  fourierdlem81  46759  fourierdlem93  46771  elaa2  46806  salexct  46906  sge00  46948  sge0f1o  46954  sge0gerp  46967  sge0lefi  46970  sge0ltfirp  46972  sge0resplit  46978  sge0iunmptlemre  46987  sge0iunmpt  46990  sge0isum  46999  sge0xp  47001  sge0reuz  47019  sge0reuzb  47020  iundjiun  47032  voliunsge0lem  47044  meaiuninc3v  47056  meaiininc2  47060  isomenndlem  47102  ovncvrrp  47136  ovnsubaddlem1  47142  hoidmvval0  47159  hoidmvlelem1  47167  vonioo  47254  vonicc  47257  smfaddlem1  47335  smfresal  47360  smfpimbor1lem2  47371  smflimmpt  47382  smfinflem  47389  smflimsuplem7  47398  smflimsuplem8  47399  smflimsupmpt  47401  smfliminfmpt  47404  ffnafv  47763  f1oresf1o2  47883  iccpartdisj  48041  mogoldbb  48405  2zrngagrp  48869  iunord  50305