Theorem rexlimd 3273

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

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

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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  r19.29af2  3274  iuneqconst  4966  reusv2lem2  5366  ralxfrALT  5382  funimassd  6977  fvelimad  6978  fvmptt  7040  dffo3f  7133  ffnfv  7146  frpoins3xpg  8187  frpoins3xp3g  8188  tz7.49  8486  nneneq  9252  ac6sfi  9306  ixpiunwdom  9614  r1val1  9823  rankuni2b  9897  infpssrlem4  10414  zorn2lem4  10607  zorn2lem5  10608  konigthlem  10683  tskuni  10898  gruiin  10925  lbzbi  13093  reuccatpfxs1  14927  iunconnlem  23778  ptbasfi  23933  alexsubALTlem3  24401  ovoliunnul  25861  iunmbl2  25911  mpteleeOLD  29506  atom1d  32988  elabreximd  33181  iundisjf  33258  esumc  34766  fvineqsneu  38539  poimirlem24  38767  poimirlem26  38769  poimirlem27  38770  heicant  38778  indexa  38872  sdclem2  38879  glbconxN  40638  cdleme26ee  41620  cdleme32d  41704  cdleme32f  41706  cdlemk38  42175  cdlemk19x  42203  cdlemk11t  42206  unielss  44423  oaun3lem1  44579  refsumcn  46263  eliuniin2  46350  rexlimd3  46374  suprnmpt  46404  disjf1o  46421  disjinfi  46422  rnmptlb  46470  rnmptbddlem  46471  rnmptbd2lem  46475  infnsuprnmpt  46477  upbdrech  46536  ssfiunibd  46540  iuneqfzuzlem  46561  infrpge  46578  xrralrecnnle  46609  supxrleubrnmpt  46631  infleinf2  46639  suprleubrnmpt  46647  infrnmptle  46648  infxrunb3rnmpt  46653  infxrgelbrnmpt  46679  iccshift  46745  iooshift  46749  fmul01lt1  46813  islptre  46846  rexlim2d  46852  limcperiod  46855  islpcn  46864  limclner  46876  fnlimfvre  46899  climinf2lem  46931  limsupmnflem  46945  limsupre3uzlem  46960  climuzlem  46968  dvnprodlem1  47171  dvnprodlem2  47172  itgperiod  47206  stoweidlem29  47254  stoweidlem31  47256  stoweidlem59  47284  stirlinglem13  47311  fourierdlem48  47379  fourierdlem51  47382  fourierdlem80  47411  fourierdlem81  47412  fourierdlem93  47424  elaa2  47459  salexct  47559  sge00  47601  sge0f1o  47607  sge0gerp  47620  sge0lefi  47623  sge0ltfirp  47625  sge0resplit  47631  sge0iunmptlemre  47640  sge0iunmpt  47643  sge0isum  47652  sge0xp  47654  sge0reuz  47672  sge0reuzb  47673  iundjiun  47685  voliunsge0lem  47697  meaiuninc3v  47709  meaiininc2  47713  isomenndlem  47755  ovncvrrp  47789  ovnsubaddlem1  47795  hoidmvval0  47812  hoidmvlelem1  47820  vonioo  47907  vonicc  47910  smfaddlem1  47988  smfresal  48013  smfpimbor1lem2  48024  smflimmpt  48035  smfinflem  48042  smflimsuplem7  48051  smflimsuplem8  48052  smflimsupmpt  48054  smfliminfmpt  48057  ffnafv  48456  f1oresf1o2  48576  iccpartdisj  48734  mogoldbb  49098  2zrngagrp  49561  iunord  51074