Theorem rexlimd 3275

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

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

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 1943  ax-6 2000  ax-7 2041  ax-12 2216

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

This theorem is used by:  r19.29af2  3276  iuneqconst  4973  reusv2lem2  5375  ralxfrALT  5391  funimassd  6954  fvelimad  6955  fvmptt  7017  dffo3f  7108  ffnfv  7121  frpoins3xpg  8145  frpoins3xp3g  8146  tz7.49  8441  nneneq  9200  ac6sfi  9254  ixpiunwdom  9562  r1val1  9768  rankuni2b  9835  infpssrlem4  10308  zorn2lem4  10501  zorn2lem5  10502  konigthlem  10571  tskuni  10786  gruiin  10813  lbzbi  12978  reuccatpfxs1  14808  iunconnlem  23621  ptbasfi  23775  alexsubALTlem3  24243  ovoliunnul  25703  iunmbl2  25753  mpteleeOLD  29282  atom1d  32742  elabreximd  32893  iundisjf  32971  esumc  34472  fvineqsneu  38098  poimirlem24  38336  poimirlem26  38338  poimirlem27  38339  heicant  38347  indexa  38425  sdclem2  38434  glbconxN  40193  cdleme26ee  41175  cdleme32d  41259  cdleme32f  41261  cdlemk38  41730  cdlemk19x  41758  cdlemk11t  41761  unielss  43986  oaun3lem1  44142  refsumcn  45791  eliuniin2  45879  rexlimd3  45903  suprnmpt  45933  disjf1o  45950  disjinfi  45951  rnmptlb  45999  rnmptbddlem  46000  rnmptbd2lem  46004  infnsuprnmpt  46006  upbdrech  46065  ssfiunibd  46069  iuneqfzuzlem  46091  infrpge  46108  xrralrecnnle  46139  supxrleubrnmpt  46161  infleinf2  46169  suprleubrnmpt  46177  infrnmptle  46178  infxrunb3rnmpt  46183  infxrgelbrnmpt  46209  iccshift  46275  iooshift  46279  fmul01lt1  46343  islptre  46376  rexlim2d  46382  limcperiod  46385  islpcn  46394  limclner  46406  fnlimfvre  46429  climinf2lem  46461  limsupmnflem  46475  limsupre3uzlem  46490  climuzlem  46498  dvnprodlem1  46701  dvnprodlem2  46702  itgperiod  46736  stoweidlem29  46784  stoweidlem31  46786  stoweidlem59  46814  stirlinglem13  46841  fourierdlem48  46909  fourierdlem51  46912  fourierdlem80  46941  fourierdlem81  46942  fourierdlem93  46954  elaa2  46989  salexct  47089  sge00  47131  sge0f1o  47137  sge0gerp  47150  sge0lefi  47153  sge0ltfirp  47155  sge0resplit  47161  sge0iunmptlemre  47170  sge0iunmpt  47173  sge0isum  47182  sge0xp  47184  sge0reuz  47202  sge0reuzb  47203  iundjiun  47215  voliunsge0lem  47227  meaiuninc3v  47239  meaiininc2  47243  isomenndlem  47285  ovncvrrp  47319  ovnsubaddlem1  47325  hoidmvval0  47342  hoidmvlelem1  47350  vonioo  47437  vonicc  47440  smfaddlem1  47518  smfresal  47543  smfpimbor1lem2  47554  smflimmpt  47565  smfinflem  47572  smflimsuplem7  47581  smflimsuplem8  47582  smflimsupmpt  47584  smfliminfmpt  47587  ffnafv  47949  f1oresf1o2  48069  iccpartdisj  48227  mogoldbb  48591  2zrngagrp  49055  iunord  50495