Theorem rexlimd 3269

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1815   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-ral 3077  df-rex 3087

This theorem is used by:  r19.29af2  3270  iuneqconst  4962  reusv2lem2  5360  ralxfrALT  5376  funimassd  6951  fvelimad  6952  fvmptt  7014  dffo3f  7106  ffnfv  7119  frpoins3xpg  8159  frpoins3xp3g  8160  tz7.49  8458  nneneq  9224  ac6sfi  9278  ixpiunwdom  9587  r1val1  9796  rankuni2b  9870  infpssrlem4  10387  zorn2lem4  10580  zorn2lem5  10581  konigthlem  10656  tskuni  10871  gruiin  10898  lbzbi  13066  reuccatpfxs1  14900  iunconnlem  23750  ptbasfi  23905  alexsubALTlem3  24373  ovoliunnul  25833  iunmbl2  25883  mpteleeOLD  29478  atom1d  32960  elabreximd  33153  iundisjf  33230  esumc  34729  fvineqsneu  38427  poimirlem24  38655  poimirlem26  38657  poimirlem27  38658  heicant  38666  indexa  38760  sdclem2  38769  glbconxN  40528  cdleme26ee  41510  cdleme32d  41594  cdleme32f  41596  cdlemk38  42065  cdlemk19x  42093  cdlemk11t  42096  unielss  44313  oaun3lem1  44469  refsumcn  46140  eliuniin2  46228  rexlimd3  46252  suprnmpt  46282  disjf1o  46299  disjinfi  46300  rnmptlb  46348  rnmptbddlem  46349  rnmptbd2lem  46353  infnsuprnmpt  46355  upbdrech  46414  ssfiunibd  46418  iuneqfzuzlem  46439  infrpge  46456  xrralrecnnle  46487  supxrleubrnmpt  46509  infleinf2  46517  suprleubrnmpt  46525  infrnmptle  46526  infxrunb3rnmpt  46531  infxrgelbrnmpt  46557  iccshift  46623  iooshift  46627  fmul01lt1  46691  islptre  46724  rexlim2d  46730  limcperiod  46733  islpcn  46742  limclner  46754  fnlimfvre  46777  climinf2lem  46809  limsupmnflem  46823  limsupre3uzlem  46838  climuzlem  46846  dvnprodlem1  47049  dvnprodlem2  47050  itgperiod  47084  stoweidlem29  47132  stoweidlem31  47134  stoweidlem59  47162  stirlinglem13  47189  fourierdlem48  47257  fourierdlem51  47260  fourierdlem80  47289  fourierdlem81  47290  fourierdlem93  47302  elaa2  47337  salexct  47437  sge00  47479  sge0f1o  47485  sge0gerp  47498  sge0lefi  47501  sge0ltfirp  47503  sge0resplit  47509  sge0iunmptlemre  47518  sge0iunmpt  47521  sge0isum  47530  sge0xp  47532  sge0reuz  47550  sge0reuzb  47551  iundjiun  47563  voliunsge0lem  47575  meaiuninc3v  47587  meaiininc2  47591  isomenndlem  47633  ovncvrrp  47667  ovnsubaddlem1  47673  hoidmvval0  47690  hoidmvlelem1  47698  vonioo  47785  vonicc  47788  smfaddlem1  47866  smfresal  47891  smfpimbor1lem2  47902  smflimmpt  47913  smfinflem  47920  smflimsuplem7  47929  smflimsuplem8  47930  smflimsupmpt  47932  smfliminfmpt  47935  ffnafv  48334  f1oresf1o2  48454  iccpartdisj  48612  mogoldbb  48976  2zrngagrp  49439  iunord  50952