Theorem rexlimd 3245

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053  df-rex 3063

This theorem is referenced by:  r19.29af2  3246  iuneqconst  4946  reusv2lem2  5336  ralxfrALT  5352  funimassd  6900  fvelimad  6901  fvmptt  6962  dffo3f  7052  ffnfv  7065  frpoins3xpg  8083  frpoins3xp3g  8084  tz7.49  8377  nneneq  9133  ac6sfi  9187  ixpiunwdom  9498  r1val1  9701  rankuni2b  9768  infpssrlem4  10219  zorn2lem4  10412  zorn2lem5  10413  konigthlem  10482  tskuni  10697  gruiin  10724  lbzbi  12877  reuccatpfxs1  14700  iunconnlem  23402  ptbasfi  23556  alexsubALTlem3  24024  ovoliunnul  25484  iunmbl2  25534  mpteleeOLD  28978  atom1d  32439  elabreximd  32595  iundisjf  32674  esumc  34211  fvineqsneu  37741  poimirlem24  37979  poimirlem26  37981  poimirlem27  37982  heicant  37990  indexa  38068  sdclem2  38077  glbconxN  39838  cdleme26ee  40820  cdleme32d  40904  cdleme32f  40906  cdlemk38  41375  cdlemk19x  41403  cdlemk11t  41406  unielss  43664  oaun3lem1  43820  refsumcn  45479  eliuniin2  45568  rexlimd3  45592  suprnmpt  45622  disjf1o  45639  disjinfi  45640  rnmptlb  45690  rnmptbddlem  45691  rnmptbd2lem  45695  infnsuprnmpt  45697  upbdrech  45756  ssfiunibd  45760  iuneqfzuzlem  45782  infrpge  45799  xrralrecnnle  45830  supxrleubrnmpt  45852  infleinf2  45860  suprleubrnmpt  45868  infrnmptle  45869  infxrunb3rnmpt  45874  infxrgelbrnmpt  45900  iccshift  45966  iooshift  45970  fmul01lt1  46034  islptre  46067  rexlim2d  46073  limcperiod  46076  islpcn  46085  limclner  46097  fnlimfvre  46120  climinf2lem  46152  limsupmnflem  46166  limsupre3uzlem  46181  climuzlem  46189  dvnprodlem1  46392  dvnprodlem2  46393  itgperiod  46427  stoweidlem29  46475  stoweidlem31  46477  stoweidlem59  46505  stirlinglem13  46532  fourierdlem48  46600  fourierdlem51  46603  fourierdlem80  46632  fourierdlem81  46633  fourierdlem93  46645  elaa2  46680  salexct  46780  sge00  46822  sge0f1o  46828  sge0gerp  46841  sge0lefi  46844  sge0ltfirp  46846  sge0resplit  46852  sge0iunmptlemre  46861  sge0iunmpt  46864  sge0isum  46873  sge0xp  46875  sge0reuz  46893  sge0reuzb  46894  iundjiun  46906  voliunsge0lem  46918  meaiuninc3v  46930  meaiininc2  46934  isomenndlem  46976  ovncvrrp  47010  ovnsubaddlem1  47016  hoidmvval0  47033  hoidmvlelem1  47041  vonioo  47128  vonicc  47131  smfaddlem1  47209  smfresal  47234  smfpimbor1lem2  47245  smflimmpt  47256  smfinflem  47263  smflimsuplem7  47272  smflimsuplem8  47273  smflimsupmpt  47275  smfliminfmpt  47278  ffnafv  47631  f1oresf1o2  47751  iccpartdisj  47909  mogoldbb  48273  2zrngagrp  48737  iunord  50163