Theorem rexlimd 3271

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

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

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 2215

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

This theorem is used by:  r19.29af2  3272  iuneqconst  4966  reusv2lem2  5368  ralxfrALT  5384  funimassd  6948  fvelimad  6949  fvmptt  7011  dffo3f  7103  ffnfv  7116  frpoins3xpg  8142  frpoins3xp3g  8143  tz7.49  8438  nneneq  9204  ac6sfi  9258  ixpiunwdom  9566  r1val1  9772  rankuni2b  9839  infpssrlem4  10312  zorn2lem4  10505  zorn2lem5  10506  konigthlem  10581  tskuni  10796  gruiin  10823  lbzbi  12989  reuccatpfxs1  14820  iunconnlem  23658  ptbasfi  23813  alexsubALTlem3  24281  ovoliunnul  25741  iunmbl2  25791  mpteleeOLD  29360  atom1d  32842  elabreximd  32993  iundisjf  33070  esumc  34569  fvineqsneu  38173  poimirlem24  38401  poimirlem26  38403  poimirlem27  38404  heicant  38412  indexa  38491  sdclem2  38500  glbconxN  40259  cdleme26ee  41241  cdleme32d  41325  cdleme32f  41327  cdlemk38  41796  cdlemk19x  41824  cdlemk11t  41827  unielss  44067  oaun3lem1  44223  refsumcn  45872  eliuniin2  45960  rexlimd3  45984  suprnmpt  46014  disjf1o  46031  disjinfi  46032  rnmptlb  46080  rnmptbddlem  46081  rnmptbd2lem  46085  infnsuprnmpt  46087  upbdrech  46146  ssfiunibd  46150  iuneqfzuzlem  46172  infrpge  46189  xrralrecnnle  46220  supxrleubrnmpt  46242  infleinf2  46250  suprleubrnmpt  46258  infrnmptle  46259  infxrunb3rnmpt  46264  infxrgelbrnmpt  46290  iccshift  46356  iooshift  46360  fmul01lt1  46424  islptre  46457  rexlim2d  46463  limcperiod  46466  islpcn  46475  limclner  46487  fnlimfvre  46510  climinf2lem  46542  limsupmnflem  46556  limsupre3uzlem  46571  climuzlem  46579  dvnprodlem1  46782  dvnprodlem2  46783  itgperiod  46817  stoweidlem29  46865  stoweidlem31  46867  stoweidlem59  46895  stirlinglem13  46922  fourierdlem48  46990  fourierdlem51  46993  fourierdlem80  47022  fourierdlem81  47023  fourierdlem93  47035  elaa2  47070  salexct  47170  sge00  47212  sge0f1o  47218  sge0gerp  47231  sge0lefi  47234  sge0ltfirp  47236  sge0resplit  47242  sge0iunmptlemre  47251  sge0iunmpt  47254  sge0isum  47263  sge0xp  47265  sge0reuz  47283  sge0reuzb  47284  iundjiun  47296  voliunsge0lem  47308  meaiuninc3v  47320  meaiininc2  47324  isomenndlem  47366  ovncvrrp  47400  ovnsubaddlem1  47406  hoidmvval0  47423  hoidmvlelem1  47431  vonioo  47518  vonicc  47521  smfaddlem1  47599  smfresal  47624  smfpimbor1lem2  47635  smflimmpt  47646  smfinflem  47653  smflimsuplem7  47662  smflimsuplem8  47663  smflimsupmpt  47665  smfliminfmpt  47668  ffnafv  48067  f1oresf1o2  48187  iccpartdisj  48345  mogoldbb  48709  2zrngagrp  49172  iunord  50610