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 1813   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

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

This theorem is referenced by:  r19.29af2  3273  iuneqconst  4969  reusv2lem2  5372  ralxfrALT  5388  funimassd  6949  fvelimad  6950  fvmptt  7012  dffo3f  7103  ffnfv  7116  frpoins3xpg  8137  frpoins3xp3g  8138  tz7.49  8433  nneneq  9191  ac6sfi  9245  ixpiunwdom  9553  r1val1  9759  rankuni2b  9826  infpssrlem4  10291  zorn2lem4  10484  zorn2lem5  10485  konigthlem  10554  tskuni  10769  gruiin  10796  lbzbi  12961  reuccatpfxs1  14786  iunconnlem  23565  ptbasfi  23719  alexsubALTlem3  24187  ovoliunnul  25647  iunmbl2  25697  mpteleeOLD  29223  atom1d  32683  elabreximd  32834  iundisjf  32912  esumc  34419  fvineqsneu  38035  poimirlem24  38273  poimirlem26  38275  poimirlem27  38276  heicant  38284  indexa  38362  sdclem2  38371  glbconxN  40130  cdleme26ee  41112  cdleme32d  41196  cdleme32f  41198  cdlemk38  41667  cdlemk19x  41695  cdlemk11t  41698  unielss  43925  oaun3lem1  44081  refsumcn  45730  eliuniin2  45818  rexlimd3  45842  suprnmpt  45872  disjf1o  45889  disjinfi  45890  rnmptlb  45938  rnmptbddlem  45939  rnmptbd2lem  45943  infnsuprnmpt  45945  upbdrech  46004  ssfiunibd  46008  iuneqfzuzlem  46030  infrpge  46047  xrralrecnnle  46078  supxrleubrnmpt  46100  infleinf2  46108  suprleubrnmpt  46116  infrnmptle  46117  infxrunb3rnmpt  46122  infxrgelbrnmpt  46148  iccshift  46214  iooshift  46218  fmul01lt1  46282  islptre  46315  rexlim2d  46321  limcperiod  46324  islpcn  46333  limclner  46345  fnlimfvre  46368  climinf2lem  46400  limsupmnflem  46414  limsupre3uzlem  46429  climuzlem  46437  dvnprodlem1  46640  dvnprodlem2  46641  itgperiod  46675  stoweidlem29  46723  stoweidlem31  46725  stoweidlem59  46753  stirlinglem13  46780  fourierdlem48  46848  fourierdlem51  46851  fourierdlem80  46880  fourierdlem81  46881  fourierdlem93  46893  elaa2  46928  salexct  47028  sge00  47070  sge0f1o  47076  sge0gerp  47089  sge0lefi  47092  sge0ltfirp  47094  sge0resplit  47100  sge0iunmptlemre  47109  sge0iunmpt  47112  sge0isum  47121  sge0xp  47123  sge0reuz  47141  sge0reuzb  47142  iundjiun  47154  voliunsge0lem  47166  meaiuninc3v  47178  meaiininc2  47182  isomenndlem  47224  ovncvrrp  47258  ovnsubaddlem1  47264  hoidmvval0  47281  hoidmvlelem1  47289  vonioo  47376  vonicc  47379  smfaddlem1  47457  smfresal  47482  smfpimbor1lem2  47493  smflimmpt  47504  smfinflem  47511  smflimsuplem7  47520  smflimsuplem8  47521  smflimsupmpt  47523  smfliminfmpt  47526  ffnafv  47885  f1oresf1o2  48005  iccpartdisj  48163  mogoldbb  48527  2zrngagrp  48991  iunord  50431